Theorem bitr4di 292

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 227	. 2 ⊢ (𝜒 ↔ 𝜃)
4	1, 3	bitrdi 290	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3bitr4g  317  bibi2i  341  mtt  368  nbn2  374  ifptru  1071  3bior1fd  1472  3biant1d  1475  clelabOLD  2896  clel4g  3575  eueq3  3625  n0moeu  4255  sbcel12  4305  sbceqg  4306  sbcne12  4309  reldisj  4348  reldisjOLD  4349  raldifeq  4387  r19.3rz  4390  ralf0  4406  eldifpr  4554  reusngf  4569  rexreusng  4574  eldiftp  4581  reusv2lem5  5271  prelpw  5307  otthg  5345  2rbropap  5421  rabxp  5569  pwvrel  5571  elrng  5731  iss  5875  elimasni  5928  eliniseg  5930  idrefALT  5945  xpcan  6005  xpcan2  6006  elpredg  6140  ordelpss  6197  fcnvres  6541  dffv3  6654  funimass4  6718  unima  6727  fndmdif  6803  fneqeql  6807  funimass3  6815  elrnrexdmb  6847  dff4  6858  fnsnb  6919  fconst4  6968  elunirn  7002  f12dfv  7022  riota1  7129  riota2df  7131  f1ocnvfv3  7146  eqfnov  7275  elrnmpores  7283  caoftrn  7442  ordsucun  7539  dflim3  7561  dfom2  7581  peano5  7604  opiota  7761  suppssr  7870  mpoxopovel  7896  brtpos  7911  rntpos  7915  ordgt0ge1  8132  ondif2  8137  oelim2  8231  omabs  8284  iiner  8379  erinxp  8381  qliftfun  8392  mapdm0  8431  ordunifi  8801  elfi2  8911  elfiun  8927  fifo  8929  noinfep  9156  cantnflem1  9185  cantnf  9189  rankonidlem  9290  r1pwALT  9308  pr2nelem  9464  cardalephex  9550  alephinit  9555  dfac5lem4  9586  cflim2  9723  cfsmolem  9730  compssiso  9834  fin1a2lem11  9870  itunisuc  9879  axdclem  9979  brdom6disj  9992  alephreg  10042  fpwwe2lem8  10098  pwfseqlem3  10120  pwfseqlem4  10122  indpi  10367  nqereu  10389  ordpinq  10403  ltanq  10431  ltmnq  10432  suplem2pr  10513  map2psrpr  10570  ssxr  10748  leltne  10768  ltneg  11178  leneg  11181  suprnub  11642  negiso  11657  elnnnn0  11977  nn0sub  11984  frnnn0fsupp  11991  zrevaddcl  12066  znnsub  12067  znn0sub  12068  prime  12102  eluz2  12288  indstr  12356  eluz2b1  12359  qrevaddcl  12411  rpneg  12462  xrleltne  12579  dfle2  12581  dflt2  12582  supxrleub  12760  infxrgelb  12769  ixxin  12796  iccid  12824  elicopnf  12877  iccsplit  12917  fzsplit2  12981  fzsn  12998  fzpr  13011  uzsplit  13028  preduz  13078  fvinim0ffz  13205  injresinj  13207  om2uzf1oi  13370  lt2sqi  13602  le2sqi  13603  hashsdom  13792  hashf1lem1  13864  hashf1lem1OLD  13865  fz1isolem  13871  prprrab  13883  ccatlcan  14127  ccatrcan  14128  s3eq3seq  14348  2swrd2eqwrdeq  14362  trclfvcotr  14416  cnpart  14647  limsuplt  14884  rlimresb  14970  mertenslem2  15289  fprod2dlem  15382  sadadd2lem2  15849  saddisjlem  15863  bitsuz  15873  gcddiv  15950  algcvgblem  15973  isprm3  16079  isprm5  16103  prmreclem5  16311  vdwapun  16365  vdwmc2  16370  ramcl  16420  pwsle  16823  ismre  16919  mreacs  16987  acsfn  16988  iscatd2  17010  cidpropd  17038  dfiso2  17101  oppcsect2  17108  isfunc  17193  setcinv  17416  lubeldm  17657  lubval  17660  glbeldm  17670  glbval  17673  tosso  17712  ipodrsfi  17839  acsfiindd  17853  imasmnd2  18014  resmndismnd  18039  submacs  18057  imasgrp2  18281  issubg  18346  resgrpisgrp  18367  subgacs  18380  eqgval  18396  gaorber  18505  symgfix2  18611  psgnran  18710  isslw  18800  sylow2alem2  18810  sylow2a  18811  sylow3lem6  18824  efgcpbllemb  18948  prmcyg  19082  gsum2d2lem  19161  gsumcom2  19163  subgdmdprd  19224  dprd2d2  19234  pgpfac1lem2  19265  pgpfac1lem4  19268  imasring  19440  drngmulne0  19592  subrgacs  19647  sdrgacs  19648  lssle0  19789  lssacs  19807  lssats2  19840  lvecvsn0  19949  islpir  20090  isnzr2  20104  zndvds  20317  znleval  20322  znleval2  20323  lindsmm  20593  islinds3  20599  islindf4  20603  ismhp3  20886  eltg2b  21659  discld  21789  opnssneib  21815  cldlp  21850  restbas  21858  leordtvallem1  21910  leordtvallem2  21911  ssidcn  21955  cnprest2  21990  lmss  21998  perfcls  22065  cmpfi  22108  1stccnp  22162  subislly  22181  hausmapdom  22200  locfindis  22230  iskgen3  22249  kgencn  22256  ptpjpre1  22271  xkoccn  22319  txrest  22331  txlm  22348  txkgen  22352  xkopt  22355  xkoinjcn  22387  imasnopn  22390  imasncld  22391  imasncls  22392  qtopcn  22414  kqfeq  22424  isr0  22437  fbfinnfr  22541  trfbas  22544  fbunfip  22569  ufileu  22619  cfinufil  22628  fmid  22660  txflf  22706  fclsrest  22724  alexsubALT  22751  tsmsres  22844  ucnima  22982  fmucndlem  22992  bldisj  23100  xmeter  23135  elbl4  23265  restmetu  23272  dscopn  23275  bl2ioo  23493  isphtpc  23695  tcphcph  23937  lmmbr2  23959  lmmbrf  23962  iscau2  23977  iscauf  23980  caucfil  23983  metcld  24006  metcld2  24007  bcthlem1  24024  bcthlem4  24027  cldcss2  24142  ovolgelb  24180  ovoliunlem1  24202  ismbfcn  24329  mbfmax  24349  mbfimaopnlem  24355  i1faddlem  24393  i1fmullem  24394  i1fres  24405  i1fpos  24406  itg1climres  24414  xrge0f  24431  itgresr  24478  iblcnlem1  24487  limcun  24594  dvres  24610  mdegmullem  24778  ply1remlem  24862  plyremlem  24999  vieta1  25007  ulmcau  25089  sineq0  25215  coseq1  25216  ang180lem3  25496  cubic  25534  atandm  25561  atandm2  25562  atandm3  25563  rlimcnp  25650  rlimcnp2  25651  vmappw  25800  dchrelbas3  25921  dchrelbas4  25926  dchrsum2  25951  bposlem6  25972  2sqreuopltb  26148  2sqreuopnnltb  26150  dchrisumlem3  26174  pntleml  26294  istrkg3ld  26354  tgcgr4  26424  lnrot2  26517  islnopp  26632  islmib  26680  brbtwn2  26798  axsegconlem6  26815  axsegcon  26820  ax5seg  26831  axpasch  26834  axeuclid  26856  axcontlem4  26860  elntg2  26878  issubgr  27160  nb3gr2nb  27273  uhgrvd00  27423  isrusgr0  27455  wlkcpr  27517  wlkcomp  27519  upgr2wlk  27557  upgrf1istrl  27592  clwlkcomp  27667  clwlkcompbp  27670  iswwlksnx  27725  wspthsnwspthsnon  27801  wspniunwspnon  27808  2pthon3v  27828  usgr2wspthons3  27849  usgr2wspthon  27850  rusgrnumwwlks  27859  clwlkclwwlklem3  27885  clwlkclwwlk  27886  clwwlknonwwlknonb  27990  0pth  28009  eupth2lem2  28103  vdgn1frgrv2  28180  fusgreg2wsp  28220  clwwlknonclwlknonf1o  28246  dlwwlknondlwlknonf1o  28249  wlkl0  28251  nmoolb  28653  nmlno0lem  28675  ubthlem1  28752  ocsh  29165  shle0  29324  eigrei  29716  adjeu  29771  nmoplb  29789  nmfnlb  29806  eleigvec2  29840  nmlnop0iALT  29877  cnlnadjlem5  29953  adjbdln  29965  jplem2  30151  cvbr2  30165  mdsl2bi  30205  chrelat3  30253  sq2reunnltb  30354  rmounid  30365  eqrrabd  30371  eqsnd  30399  nelpr  30401  disjunsn  30455  ofpreima  30526  funcnvmpt  30528  funcnv5mpt  30529  dfcnv2  30537  suppiniseg  30544  gtiso  30557  fpwrelmap  30592  infxrge0glb  30612  xrdifh  30625  fzsplit3  30639  swrdrn3  30751  toslublem  30776  tosglblem  30778  mgcval  30791  xrge0tsmsbi  30844  cntzun  30846  isarchi  30962  lsmsnorb  31100  nsgqusf1olem2  31120  isprmidl  31134  smatrcl  31267  ist0cld  31304  rspectopn  31338  zarcls  31345  rhmpreimacnlem  31355  unitdivcld  31372  lmxrge0  31423  isrrext  31469  issibf  31819  eulerpartlemr  31860  eulerpartlemmf  31861  eulerpartlemn  31867  dstfrvunirn  31960  ballotlemfc0  31978  ballotlemfcc  31979  reprsuc  32114  reprpmtf1o  32125  reprdifc  32126  bnj919  32266  bnj976  32277  bnj1542  32357  bnj150  32376  bnj151  32377  bnj607  32416  bnj852  32421  bnj873  32424  bnj938  32437  bnj1171  32500  bnj1388  32533  bnj1489  32556  nummin  32592  usgrgt2cycl  32608  subfacp1lem3  32660  subfacp1lem5  32662  erdszelem9  32677  kur14  32694  iscvm  32737  satf0op  32855  mclsax  33047  dfpo2  33238  elintfv  33254  fundmpss  33256  opelco3  33265  dfon2  33284  frxp2  33346  xpord2pred  33347  xpord2ind  33349  noetasuplem4  33504  noetainflem4  33508  addsid1  33675  dfbigcup2  33750  sscoid  33764  funpartfv  33796  dfrdg4  33802  cgr3permute3  33898  segletr  33965  segleantisym  33966  seglelin  33967  fneval  34090  neibastop3  34100  eltail  34112  filnetlem4  34119  bj-hbntbi  34432  bj-sbceqgALT  34623  bj-clel3gALT  34747  bj-rest10  34783  bj-0int  34796  topdifinffinlem  35044  isbasisrelowllem1  35052  isbasisrelowllem2  35053  rdgeqoa  35067  finxpreclem4  35091  finxpsuclem  35094  wl-ifp4impr  35164  wl-1xor  35179  uncf  35316  phpreu  35321  cos2h  35328  tan2h  35329  matunitlindflem1  35333  poimirlem16  35353  poimirlem19  35356  poimirlem23  35360  poimirlem24  35361  poimirlem26  35363  poimirlem27  35364  mbfposadd  35384  cnambfre  35385  itg2addnclem  35388  itg2addnc  35391  iblabsnclem  35400  ftc1anclem1  35410  ftc1anclem5  35414  caures  35478  heiborlem3  35531  heiborlem10  35538  elghomOLD  35605  divrngidl  35746  eqrelf  35957  brvbrvvdif  35965  eldmqsres2  35984  exanres  35992  ssrel3  35996  relcnveq  36019  iss2  36041  ecinn0  36047  brxrn2  36067  ecxrn  36079  eldmcoss2  36139  eldm1cossres  36140  elrelsrel  36167  elrelscnveq  36172  elcoeleqvrelsrel  36271  brredundsredund  36302  brdmqssqs  36322  cnvepresdmqss  36326  eldmqs1cossres  36333  brerser  36350  erim2  36351  eleldisjseldisj  36402  prtlem10  36441  prtlem16  36445  prtlem19  36454  prtex  36456  prter3  36458  islshpat  36593  lcvbr2  36598  lcvbr3  36599  lshpsmreu  36685  isat3  36883  hlrelat5N  36977  islpln5  37111  cdlemblem  37369  paddvaln0N  37377  paddval0  37386  cdlemefrs29bpre1  37973  cdlemefrs29cpre1  37974  cdlemg27b  38272  cdlemg33c  38284  cdlemg33e  38286  diaglbN  38631  cdlemm10N  38694  dicopelval2  38757  dicelval2N  38758  dihopelvalcpre  38824  dihglbcpreN  38876  dih1dimatlem  38905  dihatexv  38914  dvh4dimlem  39019  mapdpglem3  39251  hdmap14lem13  39456  hdmapglem7a  39503  fnsnbt  39714  fsuppind  39784  isnacs2  40020  rabrenfdioph  40128  expdiophlem1  40335  pw2f1ocnv  40351  pwfi2f1o  40413  numinfctb  40420  dfacbasgrp  40425  islnr3  40432  isdomn3  40521  dfhe3  40849  clsk3nimkb  41116  ntrneiiso  41167  ntrneikb  41170  scottabf  41321  mnuunid  41358  hashnzfzclim  41399  dvconstbi  41411  sbcoreleleqVD  41938  rfcnpre3  42035  rfcnpre4  42036  cncfshift  42882  stoweidlem59  43067  dfafv23  44177  nelbrnel  44200  elsetpreimafvrab  44279  iccpartiun  44319  prproropf1olem0  44387  prprelb  44401  prprspr2  44403  reuprpr  44408  oddm1evenALTV  44560  oddp1evenALTV  44561  oddprmne2  44600  fpprel  44613  submgmacs  44791  ismhm0  44792  iscmgmALT  44851  iscsgrpALT  44853  isrnghmmul  44884  elpglem2  45632