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  1075  3bior1fd  1476  3biant1d  1479  clelabOLD  2881  clel4g  3653  eueq3  3708  sbceqal  3844  n0moeu  4357  sbcel12  4409  sbceqg  4410  sbcne12  4413  reldisj  4452  reldisjOLD  4453  raldifeq  4494  r19.3rz  4497  ralf0  4514  eldifpr  4661  reusngf  4677  rexreusng  4684  eldiftp  4691  reusv2lem5  5401  prelpw  5447  otthg  5486  2rbropap  5567  rabxp  5725  pwvrel  5727  ssrel3  5787  elrng  5892  iss  6036  idrefALT  6113  xpcan  6176  xpcan2  6177  dfpo2  6296  ordelpss  6393  fcnvres  6769  dffv3  6888  funimass4  6957  unima  6967  fndmdif  7044  fneqeql  7048  funimass3  7056  elrnrexdmb  7092  dff4  7103  fnsnb  7164  fconst4  7216  elunirn  7250  f12dfv  7271  riota1  7387  riota2df  7389  f1ocnvfv3  7404  eqfnov  7538  elrnmpores  7546  caoftrn  7708  ordsucun  7813  dflim3  7836  dfom2  7857  peano5  7884  peano5OLD  7885  opiota  8045  frxp2  8130  xpord2pred  8131  xpord2indlem  8133  suppssr  8181  mpoxopovel  8205  brtpos  8220  rntpos  8224  ordgt0ge1  8493  ondif2  8502  oelim2  8595  omabs  8650  naddrid  8682  iiner  8783  erinxp  8785  qliftfun  8796  mapdm0  8836  ordunifi  9293  elfi2  9409  elfiun  9425  fifo  9427  noinfep  9655  cantnflem1  9684  cantnf  9688  rankonidlem  9823  r1pwALT  9841  pr2nelemOLD  9998  cardalephex  10085  alephinit  10090  dfac5lem4  10121  cflim2  10258  cfsmolem  10265  compssiso  10369  fin1a2lem11  10405  itunisuc  10414  axdclem  10514  brdom6disj  10527  alephreg  10577  fpwwe2lem8  10633  pwfseqlem3  10655  pwfseqlem4  10657  indpi  10902  nqereu  10924  ordpinq  10938  ltanq  10966  ltmnq  10967  suplem2pr  11048  map2psrpr  11105  ssxr  11283  leltne  11303  ltneg  11714  leneg  11717  suprnub  12179  negiso  12194  elnnnn0  12515  nn0sub  12522  fcdmnn0fsupp  12529  zrevaddcl  12607  znnsub  12608  znn0sub  12609  prime  12643  eluz2  12828  indstr  12900  eluz2b1  12903  qrevaddcl  12955  rpneg  13006  xrleltne  13124  dfle2  13126  dflt2  13127  supxrleub  13305  infxrgelb  13314  ixxin  13341  iccid  13369  elicopnf  13422  iccsplit  13462  fzsplit2  13526  fzsn  13543  fzpr  13556  uzsplit  13573  preduz  13623  fvinim0ffz  13751  injresinj  13753  om2uzf1oi  13918  lt2sqi  14153  le2sqi  14154  hashsdom  14341  hashf1lem1  14415  hashf1lem1OLD  14416  fz1isolem  14422  prprrab  14434  ccatlcan  14668  ccatrcan  14669  s3eq3seq  14890  2swrd2eqwrdeq  14904  trclfvcotr  14956  cnpart  15187  limsuplt  15423  rlimresb  15509  mertenslem2  15831  fprod2dlem  15924  sadadd2lem2  16391  saddisjlem  16405  bitsuz  16415  gcddiv  16493  algcvgblem  16514  isprm3  16620  isprm5  16644  prmreclem5  16853  vdwapun  16907  vdwmc2  16912  ramcl  16962  pwsle  17438  ismre  17534  mreacs  17602  acsfn  17603  iscatd2  17625  cidpropd  17654  dfiso2  17719  oppcsect2  17726  isfunc  17814  setcinv  18040  lubeldm  18306  lubval  18309  glbeldm  18319  glbval  18322  tosso  18372  ipodrsfi  18492  acsfiindd  18506  imasmnd2  18662  resmndismnd  18689  submacs  18708  imasgrp2  18938  issubg  19006  resgrpisgrp  19027  subgacs  19041  eqgval  19057  gaorber  19172  symgfix2  19284  psgnran  19383  isslw  19476  sylow2alem2  19486  sylow2a  19487  sylow3lem6  19500  efgcpbllemb  19623  prmcyg  19762  gsum2d2lem  19841  gsumcom2  19843  subgdmdprd  19904  dprd2d2  19914  pgpfac1lem2  19945  pgpfac1lem4  19948  imasring  20143  isnzr2  20297  drngmulne0  20387  subrgacs  20416  sdrgacs  20417  lssle0  20560  lssacs  20578  lssats2  20611  lvecvsn0  20722  islpir  20887  zndvds  21105  znleval  21110  znleval2  21111  lindsmm  21383  islinds3  21389  islindf4  21393  ismhp3  21686  eltg2b  22462  discld  22593  opnssneib  22619  cldlp  22654  restbas  22662  leordtvallem1  22714  leordtvallem2  22715  ssidcn  22759  cnprest2  22794  lmss  22802  perfcls  22869  cmpfi  22912  1stccnp  22966  subislly  22985  hausmapdom  23004  locfindis  23034  iskgen3  23053  kgencn  23060  ptpjpre1  23075  xkoccn  23123  txrest  23135  txlm  23152  txkgen  23156  xkopt  23159  xkoinjcn  23191  imasnopn  23194  imasncld  23195  imasncls  23196  qtopcn  23218  kqfeq  23228  isr0  23241  fbfinnfr  23345  trfbas  23348  fbunfip  23373  ufileu  23423  cfinufil  23432  fmid  23464  txflf  23510  fclsrest  23528  alexsubALT  23555  tsmsres  23648  ucnima  23786  fmucndlem  23796  bldisj  23904  xmeter  23939  elbl4  24072  restmetu  24079  dscopn  24082  bl2ioo  24308  isphtpc  24510  tcphcph  24754  lmmbr2  24776  lmmbrf  24779  iscau2  24794  iscauf  24797  caucfil  24800  metcld  24823  metcld2  24824  bcthlem1  24841  bcthlem4  24844  cldcss2  24959  ovolgelb  24997  ovoliunlem1  25019  ismbfcn  25146  mbfmax  25166  mbfimaopnlem  25172  i1faddlem  25210  i1fmullem  25211  i1fres  25223  i1fpos  25224  itg1climres  25232  xrge0f  25249  itgresr  25296  iblcnlem1  25305  limcun  25412  dvres  25428  mdegmullem  25596  ply1remlem  25680  plyremlem  25817  vieta1  25825  ulmcau  25907  sineq0  26033  coseq1  26034  ang180lem3  26316  cubic  26354  atandm  26381  atandm2  26382  atandm3  26383  rlimcnp  26470  rlimcnp2  26471  vmappw  26620  dchrelbas3  26741  dchrelbas4  26746  dchrsum2  26771  bposlem6  26792  2sqreuopltb  26968  2sqreuopnnltb  26970  dchrisumlem3  26994  pntleml  27114  noetasuplem4  27239  noetainflem4  27243  addsrid  27450  mulsrid  27572  istrkg3ld  27743  tgcgr4  27813  lnrot2  27906  islnopp  28021  islmib  28069  brbtwn2  28194  axsegconlem6  28211  axsegcon  28216  ax5seg  28227  axpasch  28230  axeuclid  28252  axcontlem4  28256  elntg2  28274  issubgr  28559  nb3gr2nb  28672  uhgrvd00  28822  isrusgr0  28854  wlkcpr  28917  wlkcomp  28919  upgr2wlk  28956  upgrf1istrl  28991  clwlkcomp  29067  clwlkcompbp  29070  iswwlksnx  29125  wspthsnwspthsnon  29201  wspniunwspnon  29208  2pthon3v  29228  usgr2wspthons3  29249  usgr2wspthon  29250  rusgrnumwwlks  29259  clwlkclwwlklem3  29285  clwlkclwwlk  29286  clwwlknonwwlknonb  29390  0pth  29409  eupth2lem2  29503  vdgn1frgrv2  29580  fusgreg2wsp  29620  clwwlknonclwlknonf1o  29646  dlwwlknondlwlknonf1o  29649  wlkl0  29651  nmoolb  30055  nmlno0lem  30077  ubthlem1  30154  ocsh  30567  shle0  30726  eigrei  31118  adjeu  31173  nmoplb  31191  nmfnlb  31208  eleigvec2  31242  nmlnop0iALT  31279  cnlnadjlem5  31355  adjbdln  31367  jplem2  31553  cvbr2  31567  mdsl2bi  31607  chrelat3  31655  eqelbid  31746  sq2reunnltb  31756  rmounid  31766  eqrrabd  31772  eqsnd  31797  nelpr  31799  disjunsn  31856  ofpreima  31921  funcnvmpt  31923  funcnv5mpt  31924  dfcnv2  31932  suppiniseg  31939  gtiso  31953  fpwrelmap  31989  infxrge0glb  32009  xrdifh  32022  fzsplit3  32036  swrdrn3  32150  toslublem  32173  tosglblem  32175  mgcval  32188  xrge0tsmsbi  32241  cntzun  32243  isarchi  32359  dvdsrspss  32522  rspsnasso  32523  lsmsnorb  32532  nsgqusf1olem2  32556  ghmquskerlem1  32559  isprmidl  32587  ressply1mon1p  32688  smatrcl  32807  ist0cld  32844  rspectopn  32878  zarcls  32885  rhmpreimacnlem  32895  unitdivcld  32912  lmxrge0  32963  isrrext  33011  issibf  33363  eulerpartlemr  33404  eulerpartlemmf  33405  eulerpartlemn  33411  dstfrvunirn  33504  ballotlemfc0  33522  ballotlemfcc  33523  reprsuc  33658  reprpmtf1o  33669  reprdifc  33670  bnj919  33809  bnj976  33819  bnj1542  33899  bnj150  33918  bnj151  33919  bnj607  33958  bnj852  33963  bnj873  33966  bnj938  33979  bnj1171  34042  bnj1388  34075  bnj1489  34098  nummin  34125  usgrgt2cycl  34152  subfacp1lem3  34204  subfacp1lem5  34206  erdszelem9  34221  kur14  34238  iscvm  34281  satf0op  34399  mclsax  34591  elintfv  34767  fundmpss  34769  opelco3  34777  dfon2  34795  dfbigcup2  34902  sscoid  34916  funpartfv  34948  dfrdg4  34954  cgr3permute3  35050  segletr  35117  segleantisym  35118  seglelin  35119  fneval  35285  neibastop3  35295  eltail  35307  filnetlem4  35314  bj-hbntbi  35630  bj-equsvt  35705  bj-sbceqgALT  35830  bj-clel3gALT  35977  bj-rest10  36017  bj-0int  36030  topdifinffinlem  36276  isbasisrelowllem1  36284  isbasisrelowllem2  36285  rdgeqoa  36299  finxpreclem4  36323  finxpsuclem  36326  wl-ifp4impr  36396  wl-1xor  36411  uncf  36515  phpreu  36520  cos2h  36527  tan2h  36528  matunitlindflem1  36532  poimirlem16  36552  poimirlem19  36555  poimirlem23  36559  poimirlem24  36560  poimirlem26  36562  poimirlem27  36563  mbfposadd  36583  cnambfre  36584  itg2addnclem  36587  itg2addnc  36590  iblabsnclem  36599  ftc1anclem1  36609  ftc1anclem5  36613  caures  36676  heiborlem3  36729  heiborlem10  36736  elghomOLD  36803  divrngidl  36944  eqrelf  37171  brvbrvvdif  37180  elrnres  37187  eldmqsres2  37204  exanres  37212  relcnveq  37239  iss2  37261  ecinn0  37270  brxrn2  37293  ecxrn  37305  disjressuc2  37306  eldmcoss2  37377  eldm1cossres  37378  elrelsrel  37405  elrelscnveq  37410  elcoeleqvrelsrel  37514  brredundsredund  37545  brdmqssqs  37565  cnvepresdmqss  37570  eldmqs1cossres  37577  brerser  37595  erimeq2  37596  eleldisjseldisj  37647  prtlem10  37783  prtlem16  37787  prtlem19  37796  prtex  37798  prter3  37800  islshpat  37935  lcvbr2  37940  lcvbr3  37941  lshpsmreu  38027  isat3  38225  hlrelat5N  38320  islpln5  38454  cdlemblem  38712  paddvaln0N  38720  paddval0  38729  cdlemefrs29bpre1  39316  cdlemefrs29cpre1  39317  cdlemg27b  39615  cdlemg33c  39627  cdlemg33e  39629  diaglbN  39974  cdlemm10N  40037  dicopelval2  40100  dicelval2N  40101  dihopelvalcpre  40167  dihglbcpreN  40219  dih1dimatlem  40248  dihatexv  40257  dvh4dimlem  40362  mapdpglem3  40594  hdmap14lem13  40799  hdmapglem7a  40846  fnsnbt  41099  fsuppind  41210  isnacs2  41492  rabrenfdioph  41600  expdiophlem1  41808  pw2f1ocnv  41824  pwfi2f1o  41886  numinfctb  41893  dfacbasgrp  41898  islnr3  41905  isdomn3  41994  onsupneqmaxlim0  42021  onsupnmax  42025  onsupuni  42026  tfsconcatrnss  42148  safesnsupfilb  42217  dfhe3  42574  clsk3nimkb  42839  ntrneiiso  42890  ntrneikb  42893  scottabf  43047  mnuunid  43084  hashnzfzclim  43129  dvconstbi  43141  sbcoreleleqVD  43668  rfcnpre3  43765  rfcnpre4  43766  r19.3rzf  43900  cncfshift  44638  stoweidlem59  44823  dfafv23  46009  nelbrnel  46032  elsetpreimafvrab  46110  iccpartiun  46150  prproropf1olem0  46218  prprelb  46232  prprspr2  46234  reuprpr  46239  oddm1evenALTV  46391  oddp1evenALTV  46392  oddprmne2  46431  fpprel  46444  submgmacs  46622  ismhm0  46623  iscmgmALT  46682  iscsgrpALT  46684  imasrng  46726  isrnghmmul  46739  mofeu  47562  iscnrm3  47633  joindm2  47649  meetdm2  47651  elpglem2  47805