Theorem bitr4d 282

Description: Deduction form of bitr4i 278. (Contributed by NM, 30-Jun-1993.)

Hypotheses

Ref	Expression
bitr4d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bitr4d.2	⊢ (𝜑 → (𝜃 ↔ 𝜒))

Assertion

Ref	Expression
bitr4d	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem bitr4d

Step	Hyp	Ref	Expression
1		bitr4d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bitr4d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
3	2	bicomd 222	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	1, 3	bitrd 279	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  3bitr2d  307  3bitr2rd  308  3bitr4d  311  3bitr4rd  312  bianabs  541  mpbirand  706  sb3b  2471  sbcom3  2501  sbal1  2523  sbal2  2524  2reu4lem  4522  issn  4830  disjprgw  5138  disjprg  5139  reuhypd  5414  snelpwg  5439  ordtri3  6400  ordsssuc  6453  iota1  6520  funbrfv2b  6951  dffn5  6952  feqmptdf  6964  unima  6968  dmfco  6989  fneqeql  7050  f1ompt  7116  dff13  7260  fliftcnv  7314  soisores  7330  isotr  7339  isoini  7341  caovord3  7629  releldm2  8042  fimaproj  8135  brtpos  8235  tpostpos  8246  oe1m  8560  oawordri  8565  oalimcl  8575  omlimcl  8593  omabs  8666  iserd  8745  qliftel  8813  qliftfun  8815  qliftf  8818  ecopovsym  8832  pw2f1olem  9095  mapen  9160  findcard3  9304  suppeqfsuppbi  9397  mapfien  9426  supisolem  9491  cantnflem1  9707  wemapwe  9715  rankr1clem  9838  rankr1c  9839  ranklim  9862  r1pwALT  9864  r1pwcl  9865  isfin1-2  10403  isfin1-4  10405  fin71num  10415  axdc3lem2  10469  ltmnq  10990  prlem936  11065  ltsosr  11112  ltasr  11118  xrlenlt  11304  ltxrlt  11309  letri3  11324  ne0gt0  11344  subadd  11488  ltsubadd2  11710  lesubadd2  11712  suble  11717  ltsub23  11719  ltaddpos2  11730  ltsubpos  11731  subge02  11755  ltord2  11768  leord2  11769  ltaddsublt  11866  divmul  11900  divmul3  11902  rec11r  11938  ltdiv1  12103  ltdivmul2  12116  ledivmul2  12118  ltrec  12121  ltdiv2  12125  negfi  12188  negiso  12219  nnle1eq1  12267  avgle1  12477  avgle2  12478  avgle  12479  nn0le0eq0  12525  elz2  12601  znnnlt1  12614  zleltp1  12638  difrp  13039  xrltlen  13152  dfle2  13153  xrletri3  13160  xgepnf  13171  xlemnf  13173  qbtwnre  13205  xltnegi  13222  supxrre  13333  infxrre  13342  elioo5  13408  elfz5  13520  elfzm11  13599  predfz  13653  flbi  13808  flbi2  13809  fldiv4lem1div2uz2  13828  fznnfl  13854  zmodid2  13891  2submod  13924  lt2sq  14124  le2sq  14125  sqlecan  14199  bcval5  14304  pfxsuffeqwrdeq  14675  shftfib  15046  mulre  15095  cnpart  15214  01sqrexlem6  15221  sqrmo  15225  elicc4abs  15293  abs2difabs  15308  cau4  15330  limsupgre  15452  clim2  15475  ello1mpt2  15493  lo1resb  15535  o1resb  15537  climeq  15538  climmpt2  15544  isercoll  15641  caucvgb  15653  fsumabs  15774  isumshft  15812  geomulcvg  15849  absefib  16169  dvdsval3  16229  dvdsabseq  16284  dvdsflip  16288  dvdsssfz1  16289  mod2eq1n2dvds  16318  ndvdsadd  16381  bitscmp  16407  smupvallem  16452  dvdssq  16532  lcmdvds  16573  ncoprmgcdgt1b  16616  isprm3  16648  isprm5  16672  phiprmpw  16739  prmdiv  16748  pc11  16843  pcz  16844  pockthlem  16868  prmreclem2  16880  prmreclem4  16882  prmreclem6  16884  1arith  16890  vdwapun  16937  rami  16978  ramcl  16992  pwsle  17468  ercpbllem  17524  invsym  17739  funcres2c  17884  latnle  18459  grpinvcnv  18957  subgacs  19110  eqger  19127  ghmqusker  19232  gexdvds2  19534  pgpfi1  19544  pgpfi  19554  lsmass  19618  lssnle  19623  lsmdisj3b  19639  lsmhash  19654  ablsubadd  19758  gsumval3lem2  19855  subgdmdprd  19985  pgpfac1lem2  20026  dvdsr02  20305  issubrg3  20533  drngid2  20639  sdrgunit  20678  sdrgacs  20683  lssacs  20845  isdomn3  21242  prmirred  21394  chrdvds  21450  chrcong  21451  chrnzr  21454  znleval  21482  znleval2  21483  cygznlem3  21497  frlmbas  21683  elfilspd  21731  lindfmm  21755  islindf4  21766  islindf5  21767  psrbaglefi  21859  psrbaglefiOLD  21860  coe1mul2lem1  22180  mdetunilem9  22516  isneip  23003  neiptopnei  23030  lpdifsn  23041  restopnb  23073  restopn2  23075  restdis  23076  restperf  23082  lmbr2  23157  cncls2  23171  cnprest  23187  cnprest2  23188  iscnrm2  23236  ist0-2  23242  ist1-3  23247  ishaus2  23249  cmpfi  23306  dfconn2  23317  1stccnp  23360  subislly  23379  hausmapdom  23398  tx1cn  23507  tx2cn  23508  txcnmpt  23522  txrest  23529  hauseqlcld  23544  tgqtop  23610  qtopcld  23611  ordthmeolem  23699  trfil2  23785  trfil3  23786  trnei  23790  ufildr  23829  fmfg  23847  rnelfm  23851  fmfnfm  23856  elflim  23869  flimrest  23881  cnflf  23900  cnflf2  23901  ptcmplem2  23951  ghmcnp  24013  tsmssubm  24041  iscfilu  24187  xmetgt0  24258  prdsxmetlem  24268  blcomps  24293  blcom  24294  xblpnfps  24295  xblpnf  24296  blpnf  24297  xmeter  24333  setsxms  24381  imasf1obl  24391  stdbdbl  24420  metrest  24427  metuel2  24468  dscopn  24476  xrtgioo  24716  metdstri  24761  cnmpopc  24843  iihalf2  24849  icopnfhmeo  24862  evth2  24880  lmmbr3  25182  iscau3  25200  metcld  25228  cfilucfil3  25242  srabn  25282  rrxmet  25330  minveclem4  25354  evthicc2  25383  ovolgelb  25403  shft2rab  25431  ovolshftlem1  25432  sca2rab  25435  ovolscalem1  25436  ioombl1lem4  25484  mbfmulc2lem  25570  ismbf3d  25577  mbfsup  25587  mbfinf  25588  i1f1lem  25612  i1fmulclem  25626  mbfi1fseqlem4  25642  itg2seq  25666  ditgneg  25780  limcdif  25799  limcnlp  25801  cnplimc  25810  rolle  25916  mvth  25919  dvne0  25938  lhop1lem  25940  itgsubst  25978  mdegle0  26007  deg1leb  26025  deg1le0  26041  q1peqb  26085  coemulhi  26182  dgrlt  26195  plydivlem3  26224  vieta1lem2  26240  aannenlem1  26257  ulmres  26318  reefiso  26379  pilem3  26384  ellogdm  26567  root1eq1  26684  angpieqvdlem  26754  angpieqvdlem2  26755  quad2  26765  1cubr  26768  quart  26787  rlimcnp  26891  wilthlem2  26995  isppw  27040  dvdsflsumcom  27114  fsumvma  27140  logfac2  27144  chpchtsum  27146  dchrmulcl  27176  dchrresb  27186  bclbnd  27207  bposlem1  27211  bposlem5  27215  gausslemma2dlem0c  27285  lgsquadlem1  27307  m1lgs  27315  2lgsoddprmlem2  27336  dchrisumlem3  27418  dchrisum0lem1  27443  sltval2  27583  noextenddif  27595  sleloe  27681  sletri3  27682  eqscut  27732  elmade2  27789  sltadd1  27903  negsunif  27961  sltsub1  27978  sltsubadd2d  27992  mulsproplem12  28021  sltmul2  28065  sltmul1d  28067  divsmulw  28086  sltdivmul2wd  28093  tgjustr  28272  trgcgrg  28313  lnrot1  28421  islnopp  28537  ismidb  28576  islmib  28585  axsegconlem6  28727  axeuclidlem  28767  axcontlem2  28770  axcontlem4  28772  axcontlem12  28780  ausgrusgrb  28972  nb3grpr2  29190  cplgr2v  29239  umgr2v2enb1  29334  crctcsh  29629  clwwlknonwwlknonb  29910  eupth2lems  30042  nmoreltpnf  30573  isblo2  30587  nmlnogt0  30601  phoeqi  30661  ubthlem2  30675  hire  30898  normgt0  30931  ho01i  31632  ho02i  31633  hoeq1  31634  hoeq2  31635  nmopreltpnf  31673  adjeq  31739  leop  31927  leopmul2i  31939  pjnormssi  31972  pjimai  31980  jplem1  32072  mddmd2  32113  mdslmd1lem1  32129  mdslmd1lem2  32130  superpos  32158  atnssm0  32180  dmdbr5ati  32226  disjunsn  32378  fcoinvbr  32389  ofpreima  32445  funcnv5mpt  32448  suppiniseg  32461  isoun  32476  fpwrelmapffslem  32509  fpwrelmap  32510  iocinioc2  32542  xrdifh  32543  nndiffz1  32549  xdivmul  32643  cntzsnid  32770  isarchi2  32888  erler  32974  elrsp  33080  lsmsnpridl  33102  lsmssass  33106  r1pid2  33270  finexttrb  33345  algextdeglem6  33385  algextdeglem7  33386  smatrcl  33392  rhmpreimacnlem  33480  sqsscirc2  33505  xrmulc1cn  33526  esumfsup  33684  1stmbfm  33875  2ndmbfm  33876  mbfmcnt  33883  eulerpartlems  33975  eulerpartlemd  33981  ballotlemfc0  34107  ballotlemfcc  34108  ballotlemsima  34130  ballotlemfrcn0  34144  sgn3da  34156  reprinfz1  34249  reprdifc  34254  bnj1173  34628  zltp1ne  34714  lfuhgr2  34723  erdszelem7  34802  erdszelem9  34804  iscvm  34864  cvmlift3lem4  34927  fscgr  35671  seglelin  35707  btwnoutside  35716  lineunray  35738  cldbnd  35805  isfne4  35819  fneval  35831  filnetlem4  35860  nndivsub  35936  bj-gabima  36413  dfgcd3  36798  fvineqsneu  36885  wl-sbhbt  37016  wl-sbcom2d  37023  wl-sbalnae  37024  wl-ax11-lem8  37054  sin2h  37078  cos2h  37079  matunitlindflem1  37084  matunitlindflem2  37085  matunitlindf  37086  ptrest  37087  poimirlem3  37091  poimirlem4  37092  poimirlem22  37110  poimirlem27  37115  mblfinlem3  37127  mblfinlem4  37128  ismblfin  37129  itg2addnclem  37139  itg2addnclem2  37140  itg2gt0cn  37143  iblabsnclem  37151  ftc1anclem6  37166  areacirclem2  37177  areacirclem5  37180  areacirc  37181  mettrifi  37225  drngoi  37419  eldm4  37741  exanres2  37764  disjecxrn  37856  brcoss2  37899  br1cossres2  37907  eldmcoss2  37926  eldm1cossres2  37928  brcosscnv2  37940  erimeq2  38145  disjlem19  38268  prter3  38349  islshpat  38484  lsatnle  38511  ellkr2  38558  lshpkr  38584  lkr0f2  38628  lduallkr3  38629  lkreqN  38637  cvrval2  38741  isat3  38774  glbconN  38844  glbconNOLD  38845  hlrelat5N  38869  cvrval4N  38882  atlt  38905  1cvrco  38940  pmaple  39229  isline2  39242  isline4N  39245  elpaddn0  39268  elpadd2at2  39275  cdlemkid4  40402  dia0  40520  cdlemm10N  40586  dibglbN  40634  dihmeetlem4preN  40774  dochkrshp3  40856  dvh4dimlem  40911  lcfl5  40964  mapdpglem3  41143  mapdheq  41196  hdmap1eq  41269  hdmapval2lem  41299  hdmapoc  41399  hlhillcs  41430  lcmineqlem18  41512  fsuppssind  41817  dvdsexpb  41893  renegadd  41918  resubadd  41925  mulgt0b2d  42006  fz1eqin  42180  diophin  42183  jm2.19  42405  rmxdiophlem  42427  pw2f1ocnv  42449  wepwsolem  42457  gicabl  42514  idomodle  42610  onsupmaxb  42658  cantnf2  42745  tfsconcatb0  42764  tfsnfin  42772  ntrclsfveq2  43482  ntrclsss  43484  ntrclsk4  43493  extoimad  43585  radcnvrat  43742  bcc0  43768  supxrre3rnmpt  44802  clim2f  45015  clim2f2  45049  liminfreuzlem  45181  liminfltlem  45183  xlimmnflimsup2  45231  xlimpnfliminf2  45240  xlimlimsupleliminf  45242  opprb  46404  funbrafv2b  46530  dfafn5a  46531  leaddsuble  46668  iccpartgtprec  46751  flsqrt  46924  dfeven2  46980  dfodd3  46981  lindslinindimp2lem4  47520  snlindsntor  47530  regt1loggt0  47600  elbigo2  47616  elbigolo1  47621  fldivexpfllog2  47629  nnlog2ge0lt1  47630  blenpw2m1  47643  naryfvalelwrdf  47697  isprsd  47965  functhinclem1  48038  thincciso  48046  thinciso  48057  prstcprs  48072  postc  48079

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »