Theorem bitr4di 288

Description: A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem bitr4di

Step	Hyp	Ref	Expression
1		bitr4di.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bitr4di.2	. . 3 ⊢ (𝜃 ↔ 𝜒)
3	2	bicomi 223	. 2 ⊢ (𝜒 ↔ 𝜃)
4	1, 3	bitrdi 286	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:  3bitr4g  313  bibi2i  337  mtt  364  nbn2  370  ifptru  1074  3bior1fd  1475  3biant1d  1478  clelabOLD  2880  clel4g  3651  eueq3  3706  sbceqal  3842  n0moeu  4355  sbcel12  4407  sbceqg  4408  sbcne12  4411  reldisj  4450  reldisjOLD  4451  raldifeq  4492  r19.3rz  4495  ralf0  4512  eldifpr  4659  reusngf  4675  rexreusng  4682  eldiftp  4689  reusv2lem5  5399  prelpw  5445  otthg  5484  2rbropap  5565  rabxp  5722  pwvrel  5724  ssrel3  5784  elrng  5889  iss  6033  idrefALT  6109  xpcan  6172  xpcan2  6173  dfpo2  6292  ordelpss  6389  fcnvres  6765  dffv3  6884  funimass4  6953  unima  6963  fndmdif  7040  fneqeql  7044  funimass3  7052  elrnrexdmb  7088  dff4  7099  fnsnb  7160  fconst4  7212  elunirn  7246  f12dfv  7267  riota1  7383  riota2df  7385  f1ocnvfv3  7400  eqfnov  7534  elrnmpores  7542  caoftrn  7704  ordsucun  7809  dflim3  7832  dfom2  7853  peano5  7880  peano5OLD  7881  opiota  8041  frxp2  8126  xpord2pred  8127  xpord2indlem  8129  suppssr  8177  mpoxopovel  8201  brtpos  8216  rntpos  8220  ordgt0ge1  8489  ondif2  8498  oelim2  8591  omabs  8646  naddrid  8678  iiner  8779  erinxp  8781  qliftfun  8792  mapdm0  8832  ordunifi  9289  elfi2  9405  elfiun  9421  fifo  9423  noinfep  9651  cantnflem1  9680  cantnf  9684  rankonidlem  9819  r1pwALT  9837  pr2nelemOLD  9994  cardalephex  10081  alephinit  10086  dfac5lem4  10117  cflim2  10254  cfsmolem  10261  compssiso  10365  fin1a2lem11  10401  itunisuc  10410  axdclem  10510  brdom6disj  10523  alephreg  10573  fpwwe2lem8  10629  pwfseqlem3  10651  pwfseqlem4  10653  indpi  10898  nqereu  10920  ordpinq  10934  ltanq  10962  ltmnq  10963  suplem2pr  11044  map2psrpr  11101  ssxr  11279  leltne  11299  ltneg  11710  leneg  11713  suprnub  12175  negiso  12190  elnnnn0  12511  nn0sub  12518  fcdmnn0fsupp  12525  zrevaddcl  12603  znnsub  12604  znn0sub  12605  prime  12639  eluz2  12824  indstr  12896  eluz2b1  12899  qrevaddcl  12951  rpneg  13002  xrleltne  13120  dfle2  13122  dflt2  13123  supxrleub  13301  infxrgelb  13310  ixxin  13337  iccid  13365  elicopnf  13418  iccsplit  13458  fzsplit2  13522  fzsn  13539  fzpr  13552  uzsplit  13569  preduz  13619  fvinim0ffz  13747  injresinj  13749  om2uzf1oi  13914  lt2sqi  14149  le2sqi  14150  hashsdom  14337  hashf1lem1  14411  hashf1lem1OLD  14412  fz1isolem  14418  prprrab  14430  ccatlcan  14664  ccatrcan  14665  s3eq3seq  14886  2swrd2eqwrdeq  14900  trclfvcotr  14952  cnpart  15183  limsuplt  15419  rlimresb  15505  mertenslem2  15827  fprod2dlem  15920  sadadd2lem2  16387  saddisjlem  16401  bitsuz  16411  gcddiv  16489  algcvgblem  16510  isprm3  16616  isprm5  16640  prmreclem5  16849  vdwapun  16903  vdwmc2  16908  ramcl  16958  pwsle  17434  ismre  17530  mreacs  17598  acsfn  17599  iscatd2  17621  cidpropd  17650  dfiso2  17715  oppcsect2  17722  isfunc  17810  setcinv  18036  lubeldm  18302  lubval  18305  glbeldm  18315  glbval  18318  tosso  18368  ipodrsfi  18488  acsfiindd  18502  imasmnd2  18658  resmndismnd  18685  submacs  18704  imasgrp2  18934  issubg  19000  resgrpisgrp  19021  subgacs  19035  eqgval  19051  gaorber  19166  symgfix2  19278  psgnran  19377  isslw  19470  sylow2alem2  19480  sylow2a  19481  sylow3lem6  19494  efgcpbllemb  19617  prmcyg  19756  gsum2d2lem  19835  gsumcom2  19837  subgdmdprd  19898  dprd2d2  19908  pgpfac1lem2  19939  pgpfac1lem4  19942  imasring  20136  isnzr2  20289  drngmulne0  20337  subrgacs  20408  sdrgacs  20409  lssle0  20552  lssacs  20570  lssats2  20603  lvecvsn0  20714  islpir  20879  zndvds  21096  znleval  21101  znleval2  21102  lindsmm  21374  islinds3  21380  islindf4  21384  ismhp3  21677  eltg2b  22453  discld  22584  opnssneib  22610  cldlp  22645  restbas  22653  leordtvallem1  22705  leordtvallem2  22706  ssidcn  22750  cnprest2  22785  lmss  22793  perfcls  22860  cmpfi  22903  1stccnp  22957  subislly  22976  hausmapdom  22995  locfindis  23025  iskgen3  23044  kgencn  23051  ptpjpre1  23066  xkoccn  23114  txrest  23126  txlm  23143  txkgen  23147  xkopt  23150  xkoinjcn  23182  imasnopn  23185  imasncld  23186  imasncls  23187  qtopcn  23209  kqfeq  23219  isr0  23232  fbfinnfr  23336  trfbas  23339  fbunfip  23364  ufileu  23414  cfinufil  23423  fmid  23455  txflf  23501  fclsrest  23519  alexsubALT  23546  tsmsres  23639  ucnima  23777  fmucndlem  23787  bldisj  23895  xmeter  23930  elbl4  24063  restmetu  24070  dscopn  24073  bl2ioo  24299  isphtpc  24501  tcphcph  24745  lmmbr2  24767  lmmbrf  24770  iscau2  24785  iscauf  24788  caucfil  24791  metcld  24814  metcld2  24815  bcthlem1  24832  bcthlem4  24835  cldcss2  24950  ovolgelb  24988  ovoliunlem1  25010  ismbfcn  25137  mbfmax  25157  mbfimaopnlem  25163  i1faddlem  25201  i1fmullem  25202  i1fres  25214  i1fpos  25215  itg1climres  25223  xrge0f  25240  itgresr  25287  iblcnlem1  25296  limcun  25403  dvres  25419  mdegmullem  25587  ply1remlem  25671  plyremlem  25808  vieta1  25816  ulmcau  25898  sineq0  26024  coseq1  26025  ang180lem3  26305  cubic  26343  atandm  26370  atandm2  26371  atandm3  26372  rlimcnp  26459  rlimcnp2  26460  vmappw  26609  dchrelbas3  26730  dchrelbas4  26735  dchrsum2  26760  bposlem6  26781  2sqreuopltb  26957  2sqreuopnnltb  26959  dchrisumlem3  26983  pntleml  27103  noetasuplem4  27228  noetainflem4  27232  addsrid  27437  mulsrid  27558  istrkg3ld  27701  tgcgr4  27771  lnrot2  27864  islnopp  27979  islmib  28027  brbtwn2  28152  axsegconlem6  28169  axsegcon  28174  ax5seg  28185  axpasch  28188  axeuclid  28210  axcontlem4  28214  elntg2  28232  issubgr  28517  nb3gr2nb  28630  uhgrvd00  28780  isrusgr0  28812  wlkcpr  28875  wlkcomp  28877  upgr2wlk  28914  upgrf1istrl  28949  clwlkcomp  29025  clwlkcompbp  29028  iswwlksnx  29083  wspthsnwspthsnon  29159  wspniunwspnon  29166  2pthon3v  29186  usgr2wspthons3  29207  usgr2wspthon  29208  rusgrnumwwlks  29217  clwlkclwwlklem3  29243  clwlkclwwlk  29244  clwwlknonwwlknonb  29348  0pth  29367  eupth2lem2  29461  vdgn1frgrv2  29538  fusgreg2wsp  29578  clwwlknonclwlknonf1o  29604  dlwwlknondlwlknonf1o  29607  wlkl0  29609  nmoolb  30011  nmlno0lem  30033  ubthlem1  30110  ocsh  30523  shle0  30682  eigrei  31074  adjeu  31129  nmoplb  31147  nmfnlb  31164  eleigvec2  31198  nmlnop0iALT  31235  cnlnadjlem5  31311  adjbdln  31323  jplem2  31509  cvbr2  31523  mdsl2bi  31563  chrelat3  31611  eqelbid  31702  sq2reunnltb  31712  rmounid  31722  eqrrabd  31728  eqsnd  31753  nelpr  31755  disjunsn  31812  ofpreima  31877  funcnvmpt  31879  funcnv5mpt  31880  dfcnv2  31888  suppiniseg  31895  gtiso  31909  fpwrelmap  31945  infxrge0glb  31965  xrdifh  31978  fzsplit3  31992  swrdrn3  32106  toslublem  32129  tosglblem  32131  mgcval  32144  xrge0tsmsbi  32197  cntzun  32199  isarchi  32315  dvdsrspss  32479  rspsnasso  32480  lsmsnorb  32489  nsgqusf1olem2  32513  ghmquskerlem1  32516  isprmidl  32544  ressply1mon1p  32645  smatrcl  32764  ist0cld  32801  rspectopn  32835  zarcls  32842  rhmpreimacnlem  32852  unitdivcld  32869  lmxrge0  32920  isrrext  32968  issibf  33320  eulerpartlemr  33361  eulerpartlemmf  33362  eulerpartlemn  33368  dstfrvunirn  33461  ballotlemfc0  33479  ballotlemfcc  33480  reprsuc  33615  reprpmtf1o  33626  reprdifc  33627  bnj919  33766  bnj976  33776  bnj1542  33856  bnj150  33875  bnj151  33876  bnj607  33915  bnj852  33920  bnj873  33923  bnj938  33936  bnj1171  33999  bnj1388  34032  bnj1489  34055  nummin  34082  usgrgt2cycl  34109  subfacp1lem3  34161  subfacp1lem5  34163  erdszelem9  34178  kur14  34195  iscvm  34238  satf0op  34356  mclsax  34548  elintfv  34724  fundmpss  34726  opelco3  34734  dfon2  34752  dfbigcup2  34859  sscoid  34873  funpartfv  34905  dfrdg4  34911  cgr3permute3  35007  segletr  35074  segleantisym  35075  seglelin  35076  fneval  35225  neibastop3  35235  eltail  35247  filnetlem4  35254  bj-hbntbi  35570  bj-equsvt  35645  bj-sbceqgALT  35770  bj-clel3gALT  35917  bj-rest10  35957  bj-0int  35970  topdifinffinlem  36216  isbasisrelowllem1  36224  isbasisrelowllem2  36225  rdgeqoa  36239  finxpreclem4  36263  finxpsuclem  36266  wl-ifp4impr  36336  wl-1xor  36351  uncf  36455  phpreu  36460  cos2h  36467  tan2h  36468  matunitlindflem1  36472  poimirlem16  36492  poimirlem19  36495  poimirlem23  36499  poimirlem24  36500  poimirlem26  36502  poimirlem27  36503  mbfposadd  36523  cnambfre  36524  itg2addnclem  36527  itg2addnc  36530  iblabsnclem  36539  ftc1anclem1  36549  ftc1anclem5  36553  caures  36616  heiborlem3  36669  heiborlem10  36676  elghomOLD  36743  divrngidl  36884  eqrelf  37111  brvbrvvdif  37120  elrnres  37127  eldmqsres2  37144  exanres  37152  relcnveq  37179  iss2  37201  ecinn0  37210  brxrn2  37233  ecxrn  37245  disjressuc2  37246  eldmcoss2  37317  eldm1cossres  37318  elrelsrel  37345  elrelscnveq  37350  elcoeleqvrelsrel  37454  brredundsredund  37485  brdmqssqs  37505  cnvepresdmqss  37510  eldmqs1cossres  37517  brerser  37535  erimeq2  37536  eleldisjseldisj  37587  prtlem10  37723  prtlem16  37727  prtlem19  37736  prtex  37738  prter3  37740  islshpat  37875  lcvbr2  37880  lcvbr3  37881  lshpsmreu  37967  isat3  38165  hlrelat5N  38260  islpln5  38394  cdlemblem  38652  paddvaln0N  38660  paddval0  38669  cdlemefrs29bpre1  39256  cdlemefrs29cpre1  39257  cdlemg27b  39555  cdlemg33c  39567  cdlemg33e  39569  diaglbN  39914  cdlemm10N  39977  dicopelval2  40040  dicelval2N  40041  dihopelvalcpre  40107  dihglbcpreN  40159  dih1dimatlem  40188  dihatexv  40197  dvh4dimlem  40302  mapdpglem3  40534  hdmap14lem13  40739  hdmapglem7a  40786  fnsnbt  41048  fsuppind  41159  isnacs2  41429  rabrenfdioph  41537  expdiophlem1  41745  pw2f1ocnv  41761  pwfi2f1o  41823  numinfctb  41830  dfacbasgrp  41835  islnr3  41842  isdomn3  41931  onsupneqmaxlim0  41958  onsupnmax  41962  onsupuni  41963  tfsconcatrnss  42085  safesnsupfilb  42154  dfhe3  42511  clsk3nimkb  42776  ntrneiiso  42827  ntrneikb  42830  scottabf  42984  mnuunid  43021  hashnzfzclim  43066  dvconstbi  43078  sbcoreleleqVD  43605  rfcnpre3  43702  rfcnpre4  43703  r19.3rzf  43837  cncfshift  44576  stoweidlem59  44761  dfafv23  45947  nelbrnel  45970  elsetpreimafvrab  46048  iccpartiun  46088  prproropf1olem0  46156  prprelb  46170  prprspr2  46172  reuprpr  46177  oddm1evenALTV  46329  oddp1evenALTV  46330  oddprmne2  46369  fpprel  46382  submgmacs  46560  ismhm0  46561  iscmgmALT  46620  iscsgrpALT  46622  imasrng  46664  isrnghmmul  46676  mofeu  47467  iscnrm3  47538  joindm2  47554  meetdm2  47556  elpglem2  47710