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  336  mtt  363  nbn2  369  ifptru  1072  3bior1fd  1472  3biant1d  1475  clelabOLD  2873  clel4g  3649  eueq3  3705  sbceqal  3842  n0moeu  4359  sbcel12  4413  sbceqg  4414  sbcne12  4417  reldisj  4456  reldisjOLD  4457  raldifeq  4498  r19.3rz  4501  ralf0  4518  eldifpr  4665  reusngf  4681  rexreusng  4688  eldiftp  4695  reusv2lem5  5406  prelpw  5452  otthg  5491  2rbropap  5572  rabxp  5730  pwvrel  5732  ssrel3  5792  elrng  5898  iss  6044  idrefALT  6123  xpcan  6187  xpcan2  6188  dfpo2  6307  ordelpss  6404  fcnvres  6779  dffv3  6897  funimass4  6967  unima  6977  fndmdif  7055  fneqeql  7059  funimass3  7067  elrnrexdmb  7104  dff4  7115  fnsnb  7180  fconst4  7231  elunirn  7266  f12dfv  7287  riota1  7402  riota2df  7404  f1ocnvfv3  7419  eqfnov  7555  elrnmpores  7564  caoftrn  7729  ordsucun  7834  dflim3  7857  dfom2  7878  peano5  7905  peano5OLD  7906  opiota  8073  frxp2  8158  xpord2pred  8159  xpord2indlem  8161  suppssr  8210  mpoxopovel  8235  brtpos  8250  rntpos  8254  ordgt0ge1  8523  ondif2  8532  oelim2  8625  omabs  8681  naddrid  8713  iiner  8818  erinxp  8820  qliftfun  8831  mapdm0  8871  ordunifi  9327  elfi2  9457  elfiun  9473  fifo  9475  noinfep  9703  cantnflem1  9732  cantnf  9736  rankonidlem  9871  r1pwALT  9889  pr2nelemOLD  10046  cardalephex  10133  alephinit  10138  dfac5lem4  10169  cflim2  10306  cfsmolem  10313  compssiso  10417  fin1a2lem11  10453  itunisuc  10462  axdclem  10562  brdom6disj  10575  alephreg  10625  fpwwe2lem8  10681  pwfseqlem3  10703  pwfseqlem4  10705  indpi  10950  nqereu  10972  ordpinq  10986  ltanq  11014  ltmnq  11015  suplem2pr  11096  map2psrpr  11153  ssxr  11333  leltne  11353  ltneg  11764  leneg  11767  suprnub  12231  negiso  12246  elnnnn0  12567  nn0sub  12574  fcdmnn0fsupp  12581  zrevaddcl  12659  znnsub  12660  znn0sub  12661  prime  12695  eluz2  12880  indstr  12952  eluz2b1  12955  qrevaddcl  13007  rpneg  13060  xrleltne  13178  dfle2  13180  dflt2  13181  supxrleub  13359  infxrgelb  13368  ixxin  13395  iccid  13423  elicopnf  13476  iccsplit  13516  fzsplit2  13580  fzsn  13597  fzpr  13610  uzsplit  13627  preduz  13677  fvinim0ffz  13806  injresinj  13808  om2uzf1oi  13973  lt2sqi  14207  le2sqi  14208  hashsdom  14398  hashf1lem1  14473  hashf1lem1OLD  14474  fz1isolem  14480  prprrab  14492  ccatlcan  14726  ccatrcan  14727  s3eq3seq  14948  2swrd2eqwrdeq  14962  trclfvcotr  15014  cnpart  15245  limsuplt  15481  rlimresb  15567  mertenslem2  15889  fprod2dlem  15982  sadadd2lem2  16450  saddisjlem  16464  bitsuz  16474  gcddiv  16552  algcvgblem  16578  isprm3  16684  isprm5  16708  prmreclem5  16922  vdwapun  16976  vdwmc2  16981  ramcl  17031  pwsle  17507  ismre  17603  mreacs  17671  acsfn  17672  iscatd2  17694  cidpropd  17723  dfiso2  17788  oppcsect2  17795  isfunc  17883  setcinv  18112  lubeldm  18378  lubval  18381  glbeldm  18391  glbval  18394  tosso  18444  ipodrsfi  18564  acsfiindd  18578  submgmacs  18710  imasmnd2  18764  ismhm0  18780  resmndismnd  18798  submacs  18817  imasgrp2  19049  issubg  19120  resgrpisgrp  19141  subgacs  19155  eqgval  19171  ghmqusnsglem1  19274  ghmquskerlem1  19277  gaorber  19302  symgfix2  19414  psgnran  19513  isslw  19606  sylow2alem2  19616  sylow2a  19617  sylow3lem6  19630  efgcpbllemb  19753  prmcyg  19892  gsum2d2lem  19971  gsumcom2  19973  subgdmdprd  20034  dprd2d2  20044  pgpfac1lem2  20075  pgpfac1lem4  20078  imasrng  20160  imasring  20309  isrnghmmul  20424  isnzr2  20500  isdomn3  20693  drngmulne0  20740  subrgacs  20779  sdrgacs  20780  lssle0  20927  lssacs  20944  lssats2  20977  lvecvsn0  21090  islpir  21317  zndvds  21547  znleval  21552  znleval2  21553  lindsmm  21826  islinds3  21832  islindf4  21836  ismhp3  22137  psdmul  22160  eltg2b  22953  discld  23084  opnssneib  23110  cldlp  23145  restbas  23153  leordtvallem1  23205  leordtvallem2  23206  ssidcn  23250  cnprest2  23285  lmss  23293  perfcls  23360  cmpfi  23403  1stccnp  23457  subislly  23476  hausmapdom  23495  locfindis  23525  iskgen3  23544  kgencn  23551  ptpjpre1  23566  xkoccn  23614  txrest  23626  txlm  23643  txkgen  23647  xkopt  23650  xkoinjcn  23682  imasnopn  23685  imasncld  23686  imasncls  23687  qtopcn  23709  kqfeq  23719  isr0  23732  fbfinnfr  23836  trfbas  23839  fbunfip  23864  ufileu  23914  cfinufil  23923  fmid  23955  txflf  24001  fclsrest  24019  alexsubALT  24046  tsmsres  24139  ucnima  24277  fmucndlem  24287  bldisj  24395  xmeter  24430  elbl4  24563  restmetu  24570  dscopn  24573  bl2ioo  24799  isphtpc  25011  tcphcph  25256  lmmbr2  25278  lmmbrf  25281  iscau2  25296  iscauf  25299  caucfil  25302  metcld  25325  metcld2  25326  bcthlem1  25343  bcthlem4  25346  cldcss2  25461  ovolgelb  25500  ovoliunlem1  25522  ismbfcn  25649  mbfmax  25669  mbfimaopnlem  25675  i1faddlem  25713  i1fmullem  25714  i1fres  25726  i1fpos  25727  itg1climres  25735  xrge0f  25752  itgresr  25799  iblcnlem1  25808  limcun  25915  dvres  25931  mdegmullem  26105  r1pid2  26189  ply1remlem  26192  plyremlem  26332  vieta1  26340  ulmcau  26424  sineq0  26551  coseq1  26552  ang180lem3  26839  cubic  26877  atandm  26904  atandm2  26905  atandm3  26906  rlimcnp  26993  rlimcnp2  26994  vmappw  27144  dchrelbas3  27267  dchrelbas4  27272  dchrsum2  27297  bposlem6  27318  2sqreuopltb  27494  2sqreuopnnltb  27496  dchrisumlem3  27520  pntleml  27640  noetasuplem4  27766  noetainflem4  27770  addsrid  27978  mulsrid  28114  mulsne0bd  28187  om2noseqf1o  28275  istrkg3ld  28388  tgcgr4  28458  lnrot2  28551  islnopp  28666  islmib  28714  brbtwn2  28839  axsegconlem6  28856  axsegcon  28861  ax5seg  28872  axpasch  28875  axeuclid  28897  axcontlem4  28901  elntg2  28919  issubgr  29207  nb3gr2nb  29320  uhgrvd00  29471  isrusgr0  29503  wlkcpr  29566  wlkcomp  29568  upgr2wlk  29605  upgrf1istrl  29640  clwlkcomp  29716  clwlkcompbp  29719  iswwlksnx  29774  wspthsnwspthsnon  29850  wspniunwspnon  29857  2pthon3v  29877  usgr2wspthons3  29898  usgr2wspthon  29899  rusgrnumwwlks  29908  clwlkclwwlklem3  29934  clwlkclwwlk  29935  clwwlknonwwlknonb  30039  0pth  30058  eupth2lem2  30152  vdgn1frgrv2  30229  fusgreg2wsp  30269  clwwlknonclwlknonf1o  30295  dlwwlknondlwlknonf1o  30298  wlkl0  30300  nmoolb  30704  nmlno0lem  30726  ubthlem1  30803  ocsh  31216  shle0  31375  eigrei  31767  adjeu  31822  nmoplb  31840  nmfnlb  31857  eleigvec2  31891  nmlnop0iALT  31928  cnlnadjlem5  32004  adjbdln  32016  jplem2  32202  cvbr2  32216  mdsl2bi  32256  chrelat3  32304  eqelbid  32403  sq2reunnltb  32413  rmounid  32423  eqrrabd  32429  eqsnd  32455  nelpr  32457  disjunsn  32514  ofpreima  32582  funcnvmpt  32584  funcnv5mpt  32585  dfcnv2  32593  suppiniseg  32598  gtiso  32612  fpwrelmap  32647  infxrge0glb  32669  xrdifh  32682  fzsplit3  32696  fzo0opth  32707  swrdrn3  32819  toslublem  32842  tosglblem  32844  mgcval  32857  xrge0tsmsbi  32927  cntzun  32929  isarchi  33047  dvdsrspss  33262  rspsnasso  33263  lsmsnorb  33266  nsgqusf1olem2  33289  isprmidl  33313  ressply1mon1p  33440  r1pid2OLD  33476  smatrcl  33611  ist0cld  33648  rspectopn  33682  zarcls  33689  rhmpreimacnlem  33699  unitdivcld  33716  lmxrge0  33767  isrrext  33815  issibf  34167  eulerpartlemr  34208  eulerpartlemmf  34209  eulerpartlemn  34215  dstfrvunirn  34308  ballotlemfc0  34326  ballotlemfcc  34327  reprsuc  34461  reprpmtf1o  34472  reprdifc  34473  bnj919  34612  bnj976  34622  bnj1542  34702  bnj150  34721  bnj151  34722  bnj607  34761  bnj852  34766  bnj873  34769  bnj938  34782  bnj1171  34845  bnj1388  34878  bnj1489  34901  nummin  34928  usgrgt2cycl  34958  subfacp1lem3  35010  subfacp1lem5  35012  erdszelem9  35027  kur14  35044  iscvm  35087  satf0op  35205  mclsax  35397  rexxfr3dALT  35467  elintfv  35588  fundmpss  35590  opelco3  35598  dfon2  35616  dfbigcup2  35723  sscoid  35737  funpartfv  35769  dfrdg4  35775  cgr3permute3  35871  segletr  35938  segleantisym  35939  seglelin  35940  fneval  36064  neibastop3  36074  eltail  36086  filnetlem4  36093  bj-hbntbi  36409  bj-equsvt  36484  bj-sbceqgALT  36608  bj-clel3gALT  36755  bj-rest10  36795  bj-0int  36808  topdifinffinlem  37054  isbasisrelowllem1  37062  isbasisrelowllem2  37063  rdgeqoa  37077  finxpreclem4  37101  finxpsuclem  37104  wl-ifp4impr  37174  wl-1xor  37189  uncf  37300  phpreu  37305  cos2h  37312  tan2h  37313  matunitlindflem1  37317  poimirlem16  37337  poimirlem19  37340  poimirlem23  37344  poimirlem24  37345  poimirlem26  37347  poimirlem27  37348  mbfposadd  37368  cnambfre  37369  itg2addnclem  37372  itg2addnc  37375  iblabsnclem  37384  ftc1anclem1  37394  ftc1anclem5  37398  caures  37461  heiborlem3  37514  heiborlem10  37521  elghomOLD  37588  divrngidl  37729  eqrelf  37953  brvbrvvdif  37962  elrnres  37969  eldmqsres2  37986  exanres  37993  relcnveq  38020  iss2  38042  ecinn0  38051  brxrn2  38073  ecxrn  38085  disjressuc2  38086  eldmcoss2  38157  eldm1cossres  38158  elrelsrel  38185  elrelscnveq  38190  elcoeleqvrelsrel  38294  brredundsredund  38325  brdmqssqs  38345  cnvepresdmqss  38350  eldmqs1cossres  38357  brerser  38375  erimeq2  38376  eleldisjseldisj  38427  prtlem10  38563  prtlem16  38567  prtlem19  38576  prtex  38578  prter3  38580  islshpat  38715  lcvbr2  38720  lcvbr3  38721  lshpsmreu  38807  isat3  39005  hlrelat5N  39100  islpln5  39234  cdlemblem  39492  paddvaln0N  39500  paddval0  39509  cdlemefrs29bpre1  40096  cdlemefrs29cpre1  40097  cdlemg27b  40395  cdlemg33c  40407  cdlemg33e  40409  diaglbN  40754  cdlemm10N  40817  dicopelval2  40880  dicelval2N  40881  dihopelvalcpre  40947  dihglbcpreN  40999  dih1dimatlem  41028  dihatexv  41037  dvh4dimlem  41142  mapdpglem3  41374  hdmap14lem13  41579  hdmapglem7a  41626  fnsnbt  41954  fsuppind  42062  isnacs2  42363  rabrenfdioph  42471  expdiophlem1  42679  pw2f1ocnv  42695  pwfi2f1o  42757  numinfctb  42764  dfacbasgrp  42769  islnr3  42776  onsupneqmaxlim0  42889  onsupnmax  42893  onsupuni  42894  tfsconcatrnss  43016  safesnsupfilb  43085  dfhe3  43442  clsk3nimkb  43707  ntrneiiso  43758  ntrneikb  43761  scottabf  43914  mnuunid  43951  hashnzfzclim  43996  dvconstbi  44008  sbcoreleleqVD  44535  rfcnpre3  44632  rfcnpre4  44633  r19.3rzf  44763  cncfshift  45495  stoweidlem59  45680  dfafv23  46866  nelbrnel  46889  elsetpreimafvrab  46966  iccpartiun  47006  prproropf1olem0  47074  prprelb  47088  prprspr2  47090  reuprpr  47095  oddm1evenALTV  47247  oddp1evenALTV  47248  oddprmne2  47287  fpprel  47300  dfvopnbgr2  47420  uhgrimisgrgric  47478  isgrlim  47488  iscmgmALT  47601  iscsgrpALT  47603  mofeu  48215  iscnrm3  48286  joindm2  48302  meetdm2  48304  elpglem2  48458