Theorem bitrdi 195

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 187	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bitr2di  196  bitr4di  197  3bitr3g  221  bibi2i  226  ibibr  245  biancomd  269  imanst  874  pm5.75  947  xordidc  1381  19.17  1536  alexdc  1599  nf4dc  1650  abeq2d  2270  cbvralf  2674  cbvrexf  2675  cbvreu  2678  cbvrab  2710  ceqsralt  2739  ralab2  2876  rexab2  2878  euxfr2dc  2897  reu7  2907  reu8  2908  cbvralcsf  3093  cbvrexcsf  3094  cbvreucsf  3095  cbvrabcsf  3096  ralss  3194  rexss  3195  prssg  3713  2ralunsn  3761  eluniab  3784  elintab  3818  dfiun2g  3881  dfiin2g  3882  cbvopab1  4037  cbvmpt  4059  axsep2  4083  bnd2  4134  opeqsn  4212  reusv3  4419  tfisi  4545  opeliunxp  4640  eliunxp  4724  relop  4735  eldm2g  4781  reldm0  4803  relrn0  4847  xpmlem  5005  elxp5  5073  cnvpom  5127  cbviota  5139  iota1  5148  sniota  5161  fncnv  5235  fnres  5285  brprcneu  5460  fnopfvb  5509  fvelrnb  5515  fvelimab  5523  fvopab3g  5540  eqfnfv3  5566  eqfnfv2f  5568  fvreseq  5570  fnreseql  5576  rexsupp  5590  respreima  5594  rexrn  5603  ralrn  5604  f1ompt  5617  fsn  5638  fconstfvm  5684  fconst3m  5685  fconst4m  5686  foima2  5699  rexima  5702  ralima  5703  dff13  5715  foeqcnvco  5737  fliftfun  5743  isocnv  5758  isoini  5765  f1oiso  5773  cbvriota  5787  eusvobj2  5807  oprabid  5850  eloprabga  5905  resoprab  5914  eqfnov  5924  eqfnov2  5925  ov6g  5955  funimassov  5967  ovelimab  5968  caovord2  5990  releldm2  6130  dfoprab4  6137  xporderlem  6175  poxp  6176  f1od2  6179  mpoxopovel  6185  brtpos2  6195  brtpos0  6196  rntpos  6201  dftpos3  6206  tpostpos  6208  tpossym  6220  tposoprab  6224  tfrcllemres  6306  frecabcl  6343  frecsuclem  6350  erth2  6522  qliftfun  6559  erovlem  6569  ecopovsym  6573  ecopovsymg  6576  th3qlem1  6579  mapdm0  6605  elpmg  6606  elpm2g  6607  map0e  6628  dom2lem  6714  mapsnen  6753  xpdom2  6773  xpf1o  6786  mapen  6788  ssfilem  6817  diffitest  6829  ac6sfi  6840  ss1o0el1o  6854  isoti  6948  cnvti  6960  omp1eomlem  7033  ismkvnex  7093  ltexpi  7252  ordpipqqs  7289  ltexnqq  7323  enq0enq  7346  enq0sym  7347  enq0tr  7349  nqnq0pi  7353  genipv  7424  genprndl  7436  genprndu  7437  genpdisj  7438  genpassl  7439  genpassu  7440  addcomprg  7493  mulcomprg  7495  ltnqpr  7508  ltnqpri  7509  ltexprlemm  7515  ltexprlemdisj  7521  suplocexprlemmu  7633  suplocexprlemdisj  7635  ltsrprg  7662  mulgt0sr  7693  elreal2  7745  ltresr  7754  ltresr2  7755  axprecex  7795  axpre-ltadd  7801  axpre-mulgt0  7802  axpre-mulext  7803  axpre-suploclemres  7816  subcan2  8095  negcon1  8122  negcon2  8123  lt0neg1  8338  lt0neg2  8339  le0neg1  8340  le0neg2  8341  reapirr  8447  reapmul1  8465  reapneg  8467  remulext1  8469  apti  8492  negap0  8500  divmulap2  8544  reclt1  8762  recgt1  8763  suprleubex  8820  addltmul  9064  elznn0  9177  zapne  9233  zltlen  9237  nn0lt10b  9239  nn0lt2  9240  eluz1  9438  raluz  9484  rexuz  9486  qltlen  9544  cnref1o  9554  rpnegap  9588  ltxr  9677  xlt0neg1  9737  xlt0neg2  9738  xle0neg1  9739  xle0neg2  9740  elixx1  9796  elixx3g  9800  elioo2  9820  icc0r  9825  elicc4  9839  elioopnf  9866  elioomnf  9867  iooneg  9887  iccneg  9888  iccshftr  9893  iccshftl  9895  iccdil  9897  icccntr  9899  iccf1o  9903  elfz1  9912  0fz1  9942  fzpr  9974  fzdifsuc  9978  uzsplit  9989  elfzm1b  9995  elfzp12  9996  fznn0  10010  exfzdc  10134  flqeqceilz  10212  zmodid2  10246  expap0  10444  bernneq  10533  hasheqf1o  10654  hashfacen  10702  sqrtmsq2i  11030  maxclpr  11117  minmax  11124  xrmaxlesup  11151  xrnegiso  11154  xrnegcon1d  11156  xrminmax  11157  clim0  11177  climrecvg1n  11240  summodc  11275  fsumsplit  11299  mertenslem2  11428  prodmodc  11470  fprodsplitdc  11488  fprod2dlemstep  11514  dvdsval2  11681  odd2np1lem  11757  even2n  11759  divalgb  11810  divalgmod  11812  zsupcllemstep  11826  gcddvds  11841  bezoutlemmain  11876  isprm3  11989  prmind2  11991  dvdsprime  11993  coprm  12013  prmdvdsexp  12017  sqrt2irr  12031  sqpweven  12044  2sqpwodd  12045  elrest  12345  istopon  12398  isbasis2g  12430  isbasis3g  12431  tgss2  12466  bastop1  12470  iscld  12490  ntreq0  12519  restsn  12567  restopn2  12570  lmbr  12600  cnptoprest2  12627  txbas  12645  eltx  12646  txlm  12666  ishmeo  12691  hmeoimaf1o  12701  ispsmet  12710  ismet  12731  isxmet  12732  ismet2  12741  metn0  12765  elblps  12777  elbl  12778  bdbl  12890  qtopbasss  12908  elcncf  12947  ellimc3apf  13016  sincosq1sgn  13134  sincosq2sgn  13135  cos11  13161  logrpap0b  13184  subctctexmid  13560  iooref1o  13592  iswomni0  13609