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  2697  cbvrexf  2698  cbvreu  2702  cbvrab  2736  ceqsralt  2765  ralab2  2902  rexab2  2904  euxfr2dc  2923  reu7  2933  reu8  2934  cbvralcsf  3120  cbvrexcsf  3121  cbvreucsf  3122  cbvrabcsf  3123  ralss  3222  rexss  3223  prssg  3750  2ralunsn  3799  eluniab  3822  elintab  3856  dfiun2g  3919  dfiin2g  3920  cbvopab1  4077  cbvmpt  4099  axsep2  4123  bnd2  4174  opeqsn  4253  reusv3  4461  tfisi  4587  opeliunxp  4682  eliunxp  4767  relop  4778  eldm2g  4824  reldm0  4846  relrn0  4890  restidsing  4964  xpmlem  5050  elxp5  5118  cnvpom  5172  cbviota  5184  iota1  5193  sniota  5208  fncnv  5283  fnres  5333  brprcneu  5509  fnopfvb  5558  fvelrnb  5564  fvelimab  5573  fvopab3g  5590  eqfnfv3  5616  eqfnfv2f  5618  fvreseq  5620  fnreseql  5627  rexsupp  5641  respreima  5645  rexrn  5654  ralrn  5655  f1ompt  5668  fsn  5689  fconstfvm  5735  fconst3m  5736  fconst4m  5737  foima2  5753  rexima  5756  ralima  5757  dff13  5769  foeqcnvco  5791  fliftfun  5797  isocnv  5812  isoini  5819  f1oiso  5827  cbvriota  5841  eusvobj2  5861  oprabid  5907  eloprabga  5962  resoprab  5971  eqfnov  5981  eqfnov2  5982  ov6g  6012  funimassov  6024  ovelimab  6025  caovord2  6047  releldm2  6186  dfoprab4  6193  xporderlem  6232  poxp  6233  f1od2  6236  mpoxopovel  6242  brtpos2  6252  brtpos0  6253  rntpos  6258  dftpos3  6263  tpostpos  6265  tpossym  6277  tposoprab  6281  tfrcllemres  6363  frecabcl  6400  frecsuclem  6407  erth2  6580  qliftfun  6617  erovlem  6627  ecopovsym  6631  ecopovsymg  6634  th3qlem1  6637  mapdm0  6663  elpmg  6664  elpm2g  6665  map0e  6686  dom2lem  6772  mapsnen  6811  xpdom2  6831  xpf1o  6844  mapen  6846  ssfilem  6875  diffitest  6887  ac6sfi  6898  ss1o0el1o  6912  isoti  7006  cnvti  7018  omp1eomlem  7093  ismkvnex  7153  nninfwlporlemd  7170  netap  7253  2omotaplemap  7256  ltexpi  7336  ordpipqqs  7373  ltexnqq  7407  enq0enq  7430  enq0sym  7431  enq0tr  7433  nqnq0pi  7437  genipv  7508  genprndl  7520  genprndu  7521  genpdisj  7522  genpassl  7523  genpassu  7524  addcomprg  7577  mulcomprg  7579  ltnqpr  7592  ltnqpri  7593  ltexprlemm  7599  ltexprlemdisj  7605  suplocexprlemmu  7717  suplocexprlemdisj  7719  ltsrprg  7746  mulgt0sr  7777  elreal2  7829  ltresr  7838  ltresr2  7839  axprecex  7879  axpre-ltadd  7885  axpre-mulgt0  7886  axpre-mulext  7887  axpre-suploclemres  7900  subcan2  8182  negcon1  8209  negcon2  8210  lt0neg1  8425  lt0neg2  8426  le0neg1  8427  le0neg2  8428  reapirr  8534  reapmul1  8552  reapneg  8554  remulext1  8556  apti  8579  negap0  8587  divmulap2  8633  reclt1  8853  recgt1  8854  suprleubex  8911  addltmul  9155  elznn0  9268  zapne  9327  zltlen  9331  nn0lt10b  9333  nn0lt2  9334  eluz1  9532  raluz  9578  rexuz  9580  qltlen  9640  cnref1o  9650  rpnegap  9686  ltxr  9775  xlt0neg1  9838  xlt0neg2  9839  xle0neg1  9840  xle0neg2  9841  elixx1  9897  elixx3g  9901  elioo2  9921  icc0r  9926  elicc4  9940  elioopnf  9967  elioomnf  9968  iooneg  9988  iccneg  9989  iccshftr  9994  iccshftl  9996  iccdil  9998  icccntr  10000  iccf1o  10004  elfz1  10013  0fz1  10045  fzpr  10077  fzdifsuc  10081  uzsplit  10092  elfzm1b  10098  elfzp12  10099  fznn0  10113  exfzdc  10240  flqeqceilz  10318  zmodid2  10352  expap0  10550  qsqeqor  10631  bernneq  10641  hasheqf1o  10765  hashfacen  10816  sqrtmsq2i  11144  maxclpr  11231  minmax  11238  xrmaxlesup  11267  xrnegiso  11270  xrnegcon1d  11272  xrminmax  11273  clim0  11293  climrecvg1n  11356  summodc  11391  fsumsplit  11415  mertenslem2  11544  prodmodc  11586  fprodsplitdc  11604  fprod2dlemstep  11630  dvdsval2  11797  odd2np1lem  11877  even2n  11879  divalgb  11930  divalgmod  11932  zsupcllemstep  11946  gcddvds  11964  bezoutlemmain  11999  nnwofdc  12039  isprm3  12118  prmind2  12120  dvdsprime  12122  coprm  12144  prmdvdsexp  12148  sqrt2irr  12162  sqpweven  12175  2sqpwodd  12176  pythagtriplem2  12266  pythagtrip  12283  pceu  12295  pc11  12330  elrest  12695  grpsubeq0  12956  grpsubadd  12958  issubg3  13052  isnsg  13062  eqger  13083  eqglact  13084  eqgid  13085  srgfcl  13156  dvdsrtr  13270  dvdsr02  13274  isunitd  13275  subsubrg2  13367  issubrg3  13368  istopon  13516  isbasis2g  13548  isbasis3g  13549  tgss2  13582  bastop1  13586  iscld  13606  ntreq0  13635  restsn  13683  restopn2  13686  lmbr  13716  cnptoprest2  13743  txbas  13761  eltx  13762  txlm  13782  ishmeo  13807  hmeoimaf1o  13817  ispsmet  13826  ismet  13847  isxmet  13848  ismet2  13857  metn0  13881  elblps  13893  elbl  13894  bdbl  14006  qtopbasss  14024  elcncf  14063  ellimc3apf  14132  sincosq1sgn  14250  sincosq2sgn  14251  cos11  14277  logrpap0b  14300  lgsdir2lem4  14435  m1lgs  14455  2lgsoddprmlem3  14462  2sqlem6  14470  2sqlem9  14474  2sqlem10  14475  subctctexmid  14753  iooref1o  14785  iswomni0  14802