Theorem bitrdi 196

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

Hypotheses

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

Assertion

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

Proof of Theorem bitrdi

Step	Hyp	Ref	Expression
1		bitrdi.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bitrdi.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
3	2	a1i 9	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	1, 3	bitrd 188	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bitr2di  197  bitr4di  198  3bitr3g  222  bibi2i  227  ibibr  246  biancomd  271  imanst  895  pm5.75  970  xordidc  1443  19.17  1604  alexdc  1667  nf4dc  1717  abeq2d  2343  cbvralf  2757  cbvrexf  2758  cbvreu  2764  cbvrab  2799  ceqsralt  2829  ralab2  2969  rexab2  2971  euxfr2dc  2990  reu7  3000  reu8  3001  cbvralcsf  3189  cbvrexcsf  3190  cbvreucsf  3191  cbvrabcsf  3192  ralss  3292  rexss  3293  elif  3618  prssg  3831  2ralunsn  3883  eluniab  3906  elintab  3940  dfiun2g  4003  dfiin2g  4004  cbvopab1  4163  cbvmpt  4185  axsep2  4209  bnd2  4265  opeqsn  4347  reusv3  4559  tfisi  4687  opeliunxp  4783  eliunxp  4871  relop  4882  eldm2g  4929  reldm0  4951  relrn0  4996  restidsing  5071  xpmlem  5159  elxp5  5227  cnvpom  5281  cbviota  5293  iota1  5303  sniota  5319  fncnv  5398  fnres  5451  brprcneu  5635  fnopfvb  5688  fvelrnb  5696  fvelimab  5705  fvopab3g  5722  eqfnfv3  5749  eqfnfv2f  5751  fvreseq  5753  fnreseql  5760  rexsupp  5774  respreima  5778  rexrn  5787  ralrn  5788  f1ompt  5801  fsn  5822  fconstfvm  5875  fconst3m  5876  fconst4m  5877  foima2  5897  rexima  5900  ralima  5901  dff13  5914  foeqcnvco  5936  fliftfun  5942  isocnv  5957  isoini  5964  f1oiso  5972  cbvriota  5988  riotaeqimp  6001  eusvobj2  6009  oprabid  6055  eloprabga  6113  resoprab  6122  eqfnov  6133  eqfnov2  6134  ov6g  6165  funimassov  6177  ovelimab  6178  caovord2  6200  uchoice  6305  releldm2  6353  dfoprab4  6360  xporderlem  6401  poxp  6402  f1od2  6405  mpoxopovel  6412  brtpos2  6422  brtpos0  6423  rntpos  6428  dftpos3  6433  tpostpos  6435  tpossym  6447  tposoprab  6451  tfrcllemres  6533  frecabcl  6570  frecsuclem  6577  erth2  6754  qliftfun  6791  erovlem  6801  ecopovsym  6805  ecopovsymg  6808  th3qlem1  6811  mapdm0  6837  elpmg  6838  elpm2g  6839  map0e  6860  dom2lem  6950  mapsnen  6991  xpdom2  7020  xpf1o  7035  mapen  7037  ssfilem  7067  ssfilemd  7069  diffitest  7081  ac6sfi  7092  eqsndc  7100  ss1o0el1o  7110  isoti  7211  cnvti  7223  omp1eomlem  7298  ismkvnex  7359  nninfwlporlemd  7376  en2prde  7403  netap  7478  2omotaplemap  7481  ltexpi  7562  ordpipqqs  7599  ltexnqq  7633  enq0enq  7656  enq0sym  7657  enq0tr  7659  nqnq0pi  7663  genipv  7734  genprndl  7746  genprndu  7747  genpdisj  7748  genpassl  7749  genpassu  7750  addcomprg  7803  mulcomprg  7805  ltnqpr  7818  ltnqpri  7819  ltexprlemm  7825  ltexprlemdisj  7831  suplocexprlemmu  7943  suplocexprlemdisj  7945  ltsrprg  7972  mulgt0sr  8003  elreal2  8055  ltresr  8064  ltresr2  8065  axprecex  8105  axpre-ltadd  8111  axpre-mulgt0  8112  axpre-mulext  8113  axpre-suploclemres  8126  subcan2  8409  negcon1  8436  negcon2  8437  lt0neg1  8653  lt0neg2  8654  le0neg1  8655  le0neg2  8656  reapirr  8762  reapmul1  8780  reapneg  8782  remulext1  8784  apti  8807  negap0  8815  divmulap2  8861  reclt1  9081  recgt1  9082  suprleubex  9139  addltmul  9386  elznn0  9499  zapne  9559  zltlen  9563  nn0lt10b  9565  nn0lt2  9566  eluz1  9764  raluz  9817  rexuz  9819  qltlen  9879  cnref1o  9890  rpnegap  9926  ltxr  10015  xlt0neg1  10078  xlt0neg2  10079  xle0neg1  10080  xle0neg2  10081  elixx1  10137  elixx3g  10141  elioo2  10161  icc0r  10166  elicc4  10180  elioopnf  10207  elioomnf  10208  iooneg  10228  iccneg  10229  iccshftr  10234  iccshftl  10236  iccdil  10238  icccntr  10240  iccf1o  10244  elfz1  10253  0fz1  10285  fzpr  10317  fzdifsuc  10321  uzsplit  10332  elfzm1b  10338  elfzp12  10339  fznn0  10353  exfzdc  10492  zsupcllemstep  10495  flqeqceilz  10586  zmodid2  10620  expap0  10837  qsqeqor  10918  bernneq  10928  hasheqf1o  11053  hashfacen  11106  ccatrn  11195  pfxsuffeqwrdeq  11288  wrd2ind  11313  sqrtmsq2i  11718  maxclpr  11805  minmax  11813  xrmaxlesup  11842  xrnegiso  11845  xrnegcon1d  11847  xrminmax  11848  clim0  11868  climrecvg1n  11931  summodc  11967  fsumsplit  11991  mertenslem2  12120  prodmodc  12162  fprodsplitdc  12180  fprod2dlemstep  12206  dvdsval2  12374  odd2np1lem  12456  even2n  12458  divalgb  12509  divalgmod  12511  bitsval  12527  bitsmod  12540  gcddvds  12557  bezoutlemmain  12592  nnwofdc  12632  isprm3  12713  prmind2  12715  dvdsprime  12717  coprm  12739  prmdvdsexp  12743  sqrt2irr  12757  sqpweven  12770  2sqpwodd  12771  pythagtriplem2  12862  pythagtrip  12879  pceu  12891  pc11  12927  elrest  13352  grpsubeq0  13692  grpsubadd  13694  issubg3  13802  isnsg  13812  eqger  13834  eqglact  13835  eqgid  13836  srgfcl  14010  dvdsrtr  14139  dvdsr02  14143  isunitd  14144  isrhm  14196  isrim0  14199  subsubrng2  14253  subsubrg2  14284  issubrg3  14285  opprdomnbg  14312  2idlelb  14543  mplelbascoe  14735  istopon  14766  isbasis2g  14798  isbasis3g  14799  tgss2  14832  bastop1  14836  iscld  14856  ntreq0  14885  restsn  14933  restopn2  14936  lmbr  14966  cnptoprest2  14993  txbas  15011  eltx  15012  txlm  15032  ishmeo  15057  hmeoimaf1o  15067  ispsmet  15076  ismet  15097  isxmet  15098  ismet2  15107  metn0  15131  elblps  15143  elbl  15144  bdbl  15256  qtopbasss  15274  elcncf  15326  ellimc3apf  15413  elply  15487  sincosq1sgn  15579  sincosq2sgn  15580  cos11  15606  logrpap0b  15629  lgsdir2lem4  15789  gausslemma2dlem0i  15815  lgsquadlem2  15836  m1lgs  15843  2lgsoddprmlem3  15869  2sqlem6  15878  2sqlem9  15882  2sqlem10  15883  vtxdfifiun  16177  wlkl1loop  16238  wlkv0  16249  wlklenvclwlk  16253  upgr2wlkdc  16257  isclwwlk  16274  isclwwlkng  16286  isclwwlknx  16296  clwwlkn2  16301  eupth2lem2dc  16339  eupth2lem3lem6fi  16351  2omap  16654  pw1map  16656  subctctexmid  16661  iooref1o  16705  iswomni0  16723