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  889  pm5.75  964  xordidc  1410  19.17  1570  alexdc  1633  nf4dc  1684  abeq2d  2309  cbvralf  2721  cbvrexf  2722  cbvreu  2727  cbvrab  2761  ceqsralt  2790  ralab2  2928  rexab2  2930  euxfr2dc  2949  reu7  2959  reu8  2960  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  ralss  3250  rexss  3251  prssg  3780  2ralunsn  3829  eluniab  3852  elintab  3886  dfiun2g  3949  dfiin2g  3950  cbvopab1  4107  cbvmpt  4129  axsep2  4153  bnd2  4207  opeqsn  4286  reusv3  4496  tfisi  4624  opeliunxp  4719  eliunxp  4806  relop  4817  eldm2g  4863  reldm0  4885  relrn0  4929  restidsing  5003  xpmlem  5091  elxp5  5159  cnvpom  5213  cbviota  5225  iota1  5234  sniota  5250  fncnv  5325  fnres  5377  brprcneu  5554  fnopfvb  5605  fvelrnb  5611  fvelimab  5620  fvopab3g  5637  eqfnfv3  5664  eqfnfv2f  5666  fvreseq  5668  fnreseql  5675  rexsupp  5689  respreima  5693  rexrn  5702  ralrn  5703  f1ompt  5716  fsn  5737  fconstfvm  5783  fconst3m  5784  fconst4m  5785  foima2  5801  rexima  5804  ralima  5805  dff13  5818  foeqcnvco  5840  fliftfun  5846  isocnv  5861  isoini  5868  f1oiso  5876  cbvriota  5891  eusvobj2  5911  oprabid  5957  eloprabga  6013  resoprab  6022  eqfnov  6033  eqfnov2  6034  ov6g  6065  funimassov  6077  ovelimab  6078  caovord2  6100  uchoice  6204  releldm2  6252  dfoprab4  6259  xporderlem  6298  poxp  6299  f1od2  6302  mpoxopovel  6308  brtpos2  6318  brtpos0  6319  rntpos  6324  dftpos3  6329  tpostpos  6331  tpossym  6343  tposoprab  6347  tfrcllemres  6429  frecabcl  6466  frecsuclem  6473  erth2  6648  qliftfun  6685  erovlem  6695  ecopovsym  6699  ecopovsymg  6702  th3qlem1  6705  mapdm0  6731  elpmg  6732  elpm2g  6733  map0e  6754  dom2lem  6840  mapsnen  6879  xpdom2  6899  xpf1o  6914  mapen  6916  ssfilem  6945  diffitest  6957  ac6sfi  6968  ss1o0el1o  6983  isoti  7082  cnvti  7094  omp1eomlem  7169  ismkvnex  7230  nninfwlporlemd  7247  netap  7339  2omotaplemap  7342  ltexpi  7423  ordpipqqs  7460  ltexnqq  7494  enq0enq  7517  enq0sym  7518  enq0tr  7520  nqnq0pi  7524  genipv  7595  genprndl  7607  genprndu  7608  genpdisj  7609  genpassl  7610  genpassu  7611  addcomprg  7664  mulcomprg  7666  ltnqpr  7679  ltnqpri  7680  ltexprlemm  7686  ltexprlemdisj  7692  suplocexprlemmu  7804  suplocexprlemdisj  7806  ltsrprg  7833  mulgt0sr  7864  elreal2  7916  ltresr  7925  ltresr2  7926  axprecex  7966  axpre-ltadd  7972  axpre-mulgt0  7973  axpre-mulext  7974  axpre-suploclemres  7987  subcan2  8270  negcon1  8297  negcon2  8298  lt0neg1  8514  lt0neg2  8515  le0neg1  8516  le0neg2  8517  reapirr  8623  reapmul1  8641  reapneg  8643  remulext1  8645  apti  8668  negap0  8676  divmulap2  8722  reclt1  8942  recgt1  8943  suprleubex  9000  addltmul  9247  elznn0  9360  zapne  9419  zltlen  9423  nn0lt10b  9425  nn0lt2  9426  eluz1  9624  raluz  9671  rexuz  9673  qltlen  9733  cnref1o  9744  rpnegap  9780  ltxr  9869  xlt0neg1  9932  xlt0neg2  9933  xle0neg1  9934  xle0neg2  9935  elixx1  9991  elixx3g  9995  elioo2  10015  icc0r  10020  elicc4  10034  elioopnf  10061  elioomnf  10062  iooneg  10082  iccneg  10083  iccshftr  10088  iccshftl  10090  iccdil  10092  icccntr  10094  iccf1o  10098  elfz1  10107  0fz1  10139  fzpr  10171  fzdifsuc  10175  uzsplit  10186  elfzm1b  10192  elfzp12  10193  fznn0  10207  exfzdc  10335  zsupcllemstep  10338  flqeqceilz  10429  zmodid2  10463  expap0  10680  qsqeqor  10761  bernneq  10771  hasheqf1o  10896  hashfacen  10947  sqrtmsq2i  11319  maxclpr  11406  minmax  11414  xrmaxlesup  11443  xrnegiso  11446  xrnegcon1d  11448  xrminmax  11449  clim0  11469  climrecvg1n  11532  summodc  11567  fsumsplit  11591  mertenslem2  11720  prodmodc  11762  fprodsplitdc  11780  fprod2dlemstep  11806  dvdsval2  11974  odd2np1lem  12056  even2n  12058  divalgb  12109  divalgmod  12111  bitsval  12127  bitsmod  12140  gcddvds  12157  bezoutlemmain  12192  nnwofdc  12232  isprm3  12313  prmind2  12315  dvdsprime  12317  coprm  12339  prmdvdsexp  12343  sqrt2irr  12357  sqpweven  12370  2sqpwodd  12371  pythagtriplem2  12462  pythagtrip  12479  pceu  12491  pc11  12527  elrest  12950  grpsubeq0  13290  grpsubadd  13292  issubg3  13400  isnsg  13410  eqger  13432  eqglact  13433  eqgid  13434  srgfcl  13607  dvdsrtr  13735  dvdsr02  13739  isunitd  13740  isrhm  13792  isrim0  13795  subsubrng2  13849  subsubrg2  13880  issubrg3  13881  opprdomnbg  13908  2idlelb  14139  istopon  14335  isbasis2g  14367  isbasis3g  14368  tgss2  14401  bastop1  14405  iscld  14425  ntreq0  14454  restsn  14502  restopn2  14505  lmbr  14535  cnptoprest2  14562  txbas  14580  eltx  14581  txlm  14601  ishmeo  14626  hmeoimaf1o  14636  ispsmet  14645  ismet  14666  isxmet  14667  ismet2  14676  metn0  14700  elblps  14712  elbl  14713  bdbl  14825  qtopbasss  14843  elcncf  14895  ellimc3apf  14982  elply  15056  sincosq1sgn  15148  sincosq2sgn  15149  cos11  15175  logrpap0b  15198  lgsdir2lem4  15358  gausslemma2dlem0i  15384  lgsquadlem2  15405  m1lgs  15412  2lgsoddprmlem3  15438  2sqlem6  15447  2sqlem9  15451  2sqlem10  15452  2omap  15728  subctctexmid  15733  iooref1o  15769  iswomni0  15786