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  888  pm5.75  962  xordidc  1399  19.17  1556  alexdc  1619  nf4dc  1670  abeq2d  2290  cbvralf  2696  cbvrexf  2697  cbvreu  2701  cbvrab  2735  ceqsralt  2764  ralab2  2901  rexab2  2903  euxfr2dc  2922  reu7  2932  reu8  2933  cbvralcsf  3119  cbvrexcsf  3120  cbvreucsf  3121  cbvrabcsf  3122  ralss  3221  rexss  3222  prssg  3749  2ralunsn  3798  eluniab  3821  elintab  3855  dfiun2g  3918  dfiin2g  3919  cbvopab1  4075  cbvmpt  4097  axsep2  4121  bnd2  4172  opeqsn  4251  reusv3  4459  tfisi  4585  opeliunxp  4680  eliunxp  4765  relop  4776  eldm2g  4822  reldm0  4844  relrn0  4888  restidsing  4962  xpmlem  5048  elxp5  5116  cnvpom  5170  cbviota  5182  iota1  5191  sniota  5206  fncnv  5281  fnres  5331  brprcneu  5507  fnopfvb  5556  fvelrnb  5562  fvelimab  5571  fvopab3g  5588  eqfnfv3  5614  eqfnfv2f  5616  fvreseq  5618  fnreseql  5625  rexsupp  5639  respreima  5643  rexrn  5652  ralrn  5653  f1ompt  5666  fsn  5687  fconstfvm  5733  fconst3m  5734  fconst4m  5735  foima2  5750  rexima  5753  ralima  5754  dff13  5766  foeqcnvco  5788  fliftfun  5794  isocnv  5809  isoini  5816  f1oiso  5824  cbvriota  5838  eusvobj2  5858  oprabid  5904  eloprabga  5959  resoprab  5968  eqfnov  5978  eqfnov2  5979  ov6g  6009  funimassov  6021  ovelimab  6022  caovord2  6044  releldm2  6183  dfoprab4  6190  xporderlem  6229  poxp  6230  f1od2  6233  mpoxopovel  6239  brtpos2  6249  brtpos0  6250  rntpos  6255  dftpos3  6260  tpostpos  6262  tpossym  6274  tposoprab  6278  tfrcllemres  6360  frecabcl  6397  frecsuclem  6404  erth2  6577  qliftfun  6614  erovlem  6624  ecopovsym  6628  ecopovsymg  6631  th3qlem1  6634  mapdm0  6660  elpmg  6661  elpm2g  6662  map0e  6683  dom2lem  6769  mapsnen  6808  xpdom2  6828  xpf1o  6841  mapen  6843  ssfilem  6872  diffitest  6884  ac6sfi  6895  ss1o0el1o  6909  isoti  7003  cnvti  7015  omp1eomlem  7090  ismkvnex  7150  nninfwlporlemd  7167  netap  7250  2omotaplemap  7253  ltexpi  7333  ordpipqqs  7370  ltexnqq  7404  enq0enq  7427  enq0sym  7428  enq0tr  7430  nqnq0pi  7434  genipv  7505  genprndl  7517  genprndu  7518  genpdisj  7519  genpassl  7520  genpassu  7521  addcomprg  7574  mulcomprg  7576  ltnqpr  7589  ltnqpri  7590  ltexprlemm  7596  ltexprlemdisj  7602  suplocexprlemmu  7714  suplocexprlemdisj  7716  ltsrprg  7743  mulgt0sr  7774  elreal2  7826  ltresr  7835  ltresr2  7836  axprecex  7876  axpre-ltadd  7882  axpre-mulgt0  7883  axpre-mulext  7884  axpre-suploclemres  7897  subcan2  8178  negcon1  8205  negcon2  8206  lt0neg1  8421  lt0neg2  8422  le0neg1  8423  le0neg2  8424  reapirr  8530  reapmul1  8548  reapneg  8550  remulext1  8552  apti  8575  negap0  8583  divmulap2  8629  reclt1  8849  recgt1  8850  suprleubex  8907  addltmul  9151  elznn0  9264  zapne  9323  zltlen  9327  nn0lt10b  9329  nn0lt2  9330  eluz1  9528  raluz  9574  rexuz  9576  qltlen  9636  cnref1o  9646  rpnegap  9682  ltxr  9771  xlt0neg1  9834  xlt0neg2  9835  xle0neg1  9836  xle0neg2  9837  elixx1  9893  elixx3g  9897  elioo2  9917  icc0r  9922  elicc4  9936  elioopnf  9963  elioomnf  9964  iooneg  9984  iccneg  9985  iccshftr  9990  iccshftl  9992  iccdil  9994  icccntr  9996  iccf1o  10000  elfz1  10009  0fz1  10040  fzpr  10072  fzdifsuc  10076  uzsplit  10087  elfzm1b  10093  elfzp12  10094  fznn0  10108  exfzdc  10235  flqeqceilz  10313  zmodid2  10347  expap0  10545  qsqeqor  10625  bernneq  10635  hasheqf1o  10758  hashfacen  10809  sqrtmsq2i  11137  maxclpr  11224  minmax  11231  xrmaxlesup  11260  xrnegiso  11263  xrnegcon1d  11265  xrminmax  11266  clim0  11286  climrecvg1n  11349  summodc  11384  fsumsplit  11408  mertenslem2  11537  prodmodc  11579  fprodsplitdc  11597  fprod2dlemstep  11623  dvdsval2  11790  odd2np1lem  11869  even2n  11871  divalgb  11922  divalgmod  11924  zsupcllemstep  11938  gcddvds  11956  bezoutlemmain  11991  nnwofdc  12031  isprm3  12110  prmind2  12112  dvdsprime  12114  coprm  12136  prmdvdsexp  12140  sqrt2irr  12154  sqpweven  12167  2sqpwodd  12168  pythagtriplem2  12258  pythagtrip  12275  pceu  12287  pc11  12322  elrest  12683  grpsubeq0  12888  grpsubadd  12890  issubg3  12983  isnsg  12993  eqger  13014  eqglact  13015  eqgid  13016  srgfcl  13087  dvdsrtr  13201  dvdsr02  13205  isunitd  13206  subsubrg2  13305  issubrg3  13306  istopon  13382  isbasis2g  13414  isbasis3g  13415  tgss2  13450  bastop1  13454  iscld  13474  ntreq0  13503  restsn  13551  restopn2  13554  lmbr  13584  cnptoprest2  13611  txbas  13629  eltx  13630  txlm  13650  ishmeo  13675  hmeoimaf1o  13685  ispsmet  13694  ismet  13715  isxmet  13716  ismet2  13725  metn0  13749  elblps  13761  elbl  13762  bdbl  13874  qtopbasss  13892  elcncf  13931  ellimc3apf  14000  sincosq1sgn  14118  sincosq2sgn  14119  cos11  14145  logrpap0b  14168  lgsdir2lem4  14303  2sqlem6  14327  2sqlem9  14331  2sqlem10  14332  subctctexmid  14610  iooref1o  14642  iswomni0  14659