Theorem bitr4di 289

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 287	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  314  bibi2i  338  mtt  365  nbn2  371  ifptru  1073  3bior1fd  1474  3biant1d  1477  clelabOLD  2885  clel4g  3594  eueq3  3647  sbceqal  3783  n0moeu  4291  sbcel12  4343  sbceqg  4344  sbcne12  4347  reldisj  4386  reldisjOLD  4387  raldifeq  4425  r19.3rz  4428  ralf0  4445  eldifpr  4594  reusngf  4609  rexreusng  4616  eldiftp  4623  reusv2lem5  5326  prelpw  5363  otthg  5401  2rbropap  5480  rabxp  5636  pwvrel  5638  ssrel3  5698  elrng  5803  iss  5946  idrefALT  6023  xpcan  6084  xpcan2  6085  dfpo2  6203  ordelpss  6298  fcnvres  6660  dffv3  6779  funimass4  6843  unima  6852  fndmdif  6928  fneqeql  6932  funimass3  6940  elrnrexdmb  6975  dff4  6986  fnsnb  7047  fconst4  7099  elunirn  7133  f12dfv  7154  riota1  7263  riota2df  7265  f1ocnvfv3  7280  eqfnov  7412  elrnmpores  7420  caoftrn  7580  ordsucun  7681  dflim3  7703  dfom2  7723  peano5  7749  peano5OLD  7750  opiota  7908  suppssr  8021  mpoxopovel  8045  brtpos  8060  rntpos  8064  ordgt0ge1  8332  ondif2  8341  oelim2  8435  omabs  8490  iiner  8587  erinxp  8589  qliftfun  8600  mapdm0  8639  ordunifi  9073  elfi2  9182  elfiun  9198  fifo  9200  noinfep  9427  cantnflem1  9456  cantnf  9460  rankonidlem  9595  r1pwALT  9613  pr2nelem  9769  cardalephex  9855  alephinit  9860  dfac5lem4  9891  cflim2  10028  cfsmolem  10035  compssiso  10139  fin1a2lem11  10175  itunisuc  10184  axdclem  10284  brdom6disj  10297  alephreg  10347  fpwwe2lem8  10403  pwfseqlem3  10425  pwfseqlem4  10427  indpi  10672  nqereu  10694  ordpinq  10708  ltanq  10736  ltmnq  10737  suplem2pr  10818  map2psrpr  10875  ssxr  11053  leltne  11073  ltneg  11484  leneg  11487  suprnub  11949  negiso  11964  elnnnn0  12285  nn0sub  12292  frnnn0fsupp  12299  zrevaddcl  12374  znnsub  12375  znn0sub  12376  prime  12410  eluz2  12597  indstr  12665  eluz2b1  12668  qrevaddcl  12720  rpneg  12771  xrleltne  12888  dfle2  12890  dflt2  12891  supxrleub  13069  infxrgelb  13078  ixxin  13105  iccid  13133  elicopnf  13186  iccsplit  13226  fzsplit2  13290  fzsn  13307  fzpr  13320  uzsplit  13337  preduz  13387  fvinim0ffz  13515  injresinj  13517  om2uzf1oi  13682  lt2sqi  13915  le2sqi  13916  hashsdom  14105  hashf1lem1  14177  hashf1lem1OLD  14178  fz1isolem  14184  prprrab  14196  ccatlcan  14440  ccatrcan  14441  s3eq3seq  14661  2swrd2eqwrdeq  14675  trclfvcotr  14729  cnpart  14960  limsuplt  15197  rlimresb  15283  mertenslem2  15606  fprod2dlem  15699  sadadd2lem2  16166  saddisjlem  16180  bitsuz  16190  gcddiv  16268  algcvgblem  16291  isprm3  16397  isprm5  16421  prmreclem5  16630  vdwapun  16684  vdwmc2  16689  ramcl  16739  pwsle  17212  ismre  17308  mreacs  17376  acsfn  17377  iscatd2  17399  cidpropd  17428  dfiso2  17493  oppcsect2  17500  isfunc  17588  setcinv  17814  lubeldm  18080  lubval  18083  glbeldm  18093  glbval  18096  tosso  18146  ipodrsfi  18266  acsfiindd  18280  imasmnd2  18431  resmndismnd  18456  submacs  18474  imasgrp2  18699  issubg  18764  resgrpisgrp  18785  subgacs  18798  eqgval  18814  gaorber  18923  symgfix2  19033  psgnran  19132  isslw  19222  sylow2alem2  19232  sylow2a  19233  sylow3lem6  19246  efgcpbllemb  19370  prmcyg  19504  gsum2d2lem  19583  gsumcom2  19585  subgdmdprd  19646  dprd2d2  19656  pgpfac1lem2  19687  pgpfac1lem4  19690  imasring  19867  drngmulne0  20022  subrgacs  20077  sdrgacs  20078  lssle0  20220  lssacs  20238  lssats2  20271  lvecvsn0  20380  islpir  20529  isnzr2  20543  zndvds  20766  znleval  20771  znleval2  20772  lindsmm  21044  islinds3  21050  islindf4  21054  ismhp3  21342  eltg2b  22118  discld  22249  opnssneib  22275  cldlp  22310  restbas  22318  leordtvallem1  22370  leordtvallem2  22371  ssidcn  22415  cnprest2  22450  lmss  22458  perfcls  22525  cmpfi  22568  1stccnp  22622  subislly  22641  hausmapdom  22660  locfindis  22690  iskgen3  22709  kgencn  22716  ptpjpre1  22731  xkoccn  22779  txrest  22791  txlm  22808  txkgen  22812  xkopt  22815  xkoinjcn  22847  imasnopn  22850  imasncld  22851  imasncls  22852  qtopcn  22874  kqfeq  22884  isr0  22897  fbfinnfr  23001  trfbas  23004  fbunfip  23029  ufileu  23079  cfinufil  23088  fmid  23120  txflf  23166  fclsrest  23184  alexsubALT  23211  tsmsres  23304  ucnima  23442  fmucndlem  23452  bldisj  23560  xmeter  23595  elbl4  23728  restmetu  23735  dscopn  23738  bl2ioo  23964  isphtpc  24166  tcphcph  24410  lmmbr2  24432  lmmbrf  24435  iscau2  24450  iscauf  24453  caucfil  24456  metcld  24479  metcld2  24480  bcthlem1  24497  bcthlem4  24500  cldcss2  24615  ovolgelb  24653  ovoliunlem1  24675  ismbfcn  24802  mbfmax  24822  mbfimaopnlem  24828  i1faddlem  24866  i1fmullem  24867  i1fres  24879  i1fpos  24880  itg1climres  24888  xrge0f  24905  itgresr  24952  iblcnlem1  24961  limcun  25068  dvres  25084  mdegmullem  25252  ply1remlem  25336  plyremlem  25473  vieta1  25481  ulmcau  25563  sineq0  25689  coseq1  25690  ang180lem3  25970  cubic  26008  atandm  26035  atandm2  26036  atandm3  26037  rlimcnp  26124  rlimcnp2  26125  vmappw  26274  dchrelbas3  26395  dchrelbas4  26400  dchrsum2  26425  bposlem6  26446  2sqreuopltb  26622  2sqreuopnnltb  26624  dchrisumlem3  26648  pntleml  26768  istrkg3ld  26831  tgcgr4  26901  lnrot2  26994  islnopp  27109  islmib  27157  brbtwn2  27282  axsegconlem6  27299  axsegcon  27304  ax5seg  27315  axpasch  27318  axeuclid  27340  axcontlem4  27344  elntg2  27362  issubgr  27647  nb3gr2nb  27760  uhgrvd00  27910  isrusgr0  27942  wlkcpr  28005  wlkcomp  28007  upgr2wlk  28045  upgrf1istrl  28080  clwlkcomp  28156  clwlkcompbp  28159  iswwlksnx  28214  wspthsnwspthsnon  28290  wspniunwspnon  28297  2pthon3v  28317  usgr2wspthons3  28338  usgr2wspthon  28339  rusgrnumwwlks  28348  clwlkclwwlklem3  28374  clwlkclwwlk  28375  clwwlknonwwlknonb  28479  0pth  28498  eupth2lem2  28592  vdgn1frgrv2  28669  fusgreg2wsp  28709  clwwlknonclwlknonf1o  28735  dlwwlknondlwlknonf1o  28738  wlkl0  28740  nmoolb  29142  nmlno0lem  29164  ubthlem1  29241  ocsh  29654  shle0  29813  eigrei  30205  adjeu  30260  nmoplb  30278  nmfnlb  30295  eleigvec2  30329  nmlnop0iALT  30366  cnlnadjlem5  30442  adjbdln  30454  jplem2  30640  cvbr2  30654  mdsl2bi  30694  chrelat3  30742  sq2reunnltb  30842  rmounid  30852  eqrrabd  30858  eqsnd  30886  nelpr  30888  disjunsn  30942  ofpreima  31011  funcnvmpt  31013  funcnv5mpt  31014  dfcnv2  31022  suppiniseg  31029  gtiso  31042  fpwrelmap  31077  infxrge0glb  31097  xrdifh  31110  fzsplit3  31124  swrdrn3  31236  toslublem  31259  tosglblem  31261  mgcval  31274  xrge0tsmsbi  31327  cntzun  31329  isarchi  31445  lsmsnorb  31588  nsgqusf1olem2  31608  isprmidl  31622  smatrcl  31755  ist0cld  31792  rspectopn  31826  zarcls  31833  rhmpreimacnlem  31843  unitdivcld  31860  lmxrge0  31911  isrrext  31959  issibf  32309  eulerpartlemr  32350  eulerpartlemmf  32351  eulerpartlemn  32357  dstfrvunirn  32450  ballotlemfc0  32468  ballotlemfcc  32469  reprsuc  32604  reprpmtf1o  32615  reprdifc  32616  bnj919  32756  bnj976  32766  bnj1542  32846  bnj150  32865  bnj151  32866  bnj607  32905  bnj852  32910  bnj873  32913  bnj938  32926  bnj1171  32989  bnj1388  33022  bnj1489  33045  nummin  33072  usgrgt2cycl  33101  subfacp1lem3  33153  subfacp1lem5  33155  erdszelem9  33170  kur14  33187  iscvm  33230  satf0op  33348  mclsax  33540  elintfv  33747  fundmpss  33749  opelco3  33758  dfon2  33777  frxp2  33800  xpord2pred  33801  xpord2ind  33803  xpord3ind  33809  naddid1  33845  noetasuplem4  33948  noetainflem4  33952  addsid1  34136  dfbigcup2  34210  sscoid  34224  funpartfv  34256  dfrdg4  34262  cgr3permute3  34358  segletr  34425  segleantisym  34426  seglelin  34427  fneval  34550  neibastop3  34560  eltail  34572  filnetlem4  34579  bj-hbntbi  34895  bj-equsvt  34970  bj-sbceqgALT  35096  bj-clel3gALT  35230  bj-rest10  35268  bj-0int  35281  topdifinffinlem  35527  isbasisrelowllem1  35535  isbasisrelowllem2  35536  rdgeqoa  35550  finxpreclem4  35574  finxpsuclem  35577  wl-ifp4impr  35647  wl-1xor  35662  uncf  35765  phpreu  35770  cos2h  35777  tan2h  35778  matunitlindflem1  35782  poimirlem16  35802  poimirlem19  35805  poimirlem23  35809  poimirlem24  35810  poimirlem26  35812  poimirlem27  35813  mbfposadd  35833  cnambfre  35834  itg2addnclem  35837  itg2addnc  35840  iblabsnclem  35849  ftc1anclem1  35859  ftc1anclem5  35863  caures  35927  heiborlem3  35980  heiborlem10  35987  elghomOLD  36054  divrngidl  36195  eqrelf  36403  brvbrvvdif  36411  eldmqsres2  36430  exanres  36438  relcnveq  36464  iss2  36486  ecinn0  36492  brxrn2  36512  ecxrn  36524  eldmcoss2  36584  eldm1cossres  36585  elrelsrel  36612  elrelscnveq  36617  elcoeleqvrelsrel  36716  brredundsredund  36747  brdmqssqs  36767  cnvepresdmqss  36771  eldmqs1cossres  36778  brerser  36795  erim2  36796  eleldisjseldisj  36847  prtlem10  36886  prtlem16  36890  prtlem19  36899  prtex  36901  prter3  36903  islshpat  37038  lcvbr2  37043  lcvbr3  37044  lshpsmreu  37130  isat3  37328  hlrelat5N  37422  islpln5  37556  cdlemblem  37814  paddvaln0N  37822  paddval0  37831  cdlemefrs29bpre1  38418  cdlemefrs29cpre1  38419  cdlemg27b  38717  cdlemg33c  38729  cdlemg33e  38731  diaglbN  39076  cdlemm10N  39139  dicopelval2  39202  dicelval2N  39203  dihopelvalcpre  39269  dihglbcpreN  39321  dih1dimatlem  39350  dihatexv  39359  dvh4dimlem  39464  mapdpglem3  39696  hdmap14lem13  39901  hdmapglem7a  39948  fnsnbt  40215  fsuppind  40286  isnacs2  40535  rabrenfdioph  40643  expdiophlem1  40850  pw2f1ocnv  40866  pwfi2f1o  40928  numinfctb  40935  dfacbasgrp  40940  islnr3  40947  isdomn3  41036  dfhe3  41390  clsk3nimkb  41657  ntrneiiso  41708  ntrneikb  41711  scottabf  41865  mnuunid  41902  hashnzfzclim  41947  dvconstbi  41959  sbcoreleleqVD  42486  rfcnpre3  42583  rfcnpre4  42584  cncfshift  43422  stoweidlem59  43607  dfafv23  44756  nelbrnel  44779  elsetpreimafvrab  44857  iccpartiun  44897  prproropf1olem0  44965  prprelb  44979  prprspr2  44981  reuprpr  44986  oddm1evenALTV  45138  oddp1evenALTV  45139  oddprmne2  45178  fpprel  45191  submgmacs  45369  ismhm0  45370  iscmgmALT  45429  iscsgrpALT  45431  isrnghmmul  45462  mofeu  46186  iscnrm3  46257  joindm2  46273  meetdm2  46275  elpglem2  46428