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  896  pm5.75  971  xordidc  1444  19.17  1605  alexdc  1668  nf4dc  1718  abeq2d  2345  eqabrd  2370  cbvralf  2768  cbvrexf  2769  cbvreu  2775  cbvrab  2810  ceqsralt  2840  ralab2  2980  rexab2  2982  euxfr2dc  3001  reu7  3011  reu8  3012  cbvralcsf  3200  cbvrexcsf  3201  cbvreucsf  3202  cbvrabcsf  3203  ralss  3303  rexss  3304  elif  3633  prssg  3850  2ralunsn  3902  eluniab  3925  elintab  3959  dfiun2g  4022  dfiin2g  4023  cbvopab1  4182  cbvmpt  4204  axsep2  4228  bnd2  4285  opeqsn  4368  reusv3  4580  tfisi  4708  opeliunxp  4804  eliunxp  4893  relop  4904  eldm2g  4951  reldm0  4973  relrn0  5018  restidsing  5093  xpmlem  5182  elxp5  5250  cnvpom  5304  cbviota  5316  iota1  5326  sniota  5342  fncnv  5421  fnres  5474  brprcneu  5662  fnopfvb  5715  fvelrnb  5723  fvelimab  5732  fvopab3g  5749  eqfnfv3  5776  eqfnfv2f  5778  fvreseq  5780  fnreseql  5787  respreima  5804  rexrn  5813  ralrn  5814  f1ompt  5827  fsn  5848  fconstfvm  5901  fconst3m  5902  fconst4m  5903  foima2  5923  rexima  5926  ralima  5927  dff13  5940  foeqcnvco  5962  fliftfun  5968  isocnv  5983  isoini  5990  f1oiso  5998  cbvriota  6014  riotaeqimp  6027  eusvobj2  6035  oprabid  6081  eloprabga  6139  resoprab  6148  eqfnov  6159  eqfnov2  6160  ov6g  6191  funimassov  6203  ovelimab  6204  caovord2  6226  uchoice  6330  releldm2  6378  dfoprab4  6385  xporderlem  6426  poxp  6427  f1od2  6430  elsuppfng  6441  elsuppfn  6442  rexsupp  6452  mpoxopovel  6471  brtpos2  6481  brtpos0  6482  rntpos  6487  dftpos3  6492  tpostpos  6494  tpossym  6506  tposoprab  6510  tfrcllemres  6592  frecabcl  6629  frecsuclem  6636  erth2  6813  qliftfun  6850  erovlem  6860  ecopovsym  6864  ecopovsymg  6867  th3qlem1  6870  mapdm0  6896  elpmg  6897  elpm2g  6898  map0e  6919  dom2lem  7010  mapsnend  7051  mapsnen  7052  xpdom2  7081  xpf1o  7096  mapen  7098  ssfilem  7129  ssfilemd  7131  diffitest  7143  ac6sfi  7154  eqsndc  7162  ss1o0el1o  7172  2omap  7268  isoti  7297  cnvti  7309  omp1eomlem  7384  ismkvnex  7445  nninfwlporlemd  7462  en2prde  7489  netap  7564  2omotaplemap  7567  ltexpi  7648  ordpipqqs  7685  ltexnqq  7719  enq0enq  7742  enq0sym  7743  enq0tr  7745  nqnq0pi  7749  genipv  7820  genprndl  7832  genprndu  7833  genpdisj  7834  genpassl  7835  genpassu  7836  addcomprg  7889  mulcomprg  7891  ltnqpr  7904  ltnqpri  7905  ltexprlemm  7911  ltexprlemdisj  7917  suplocexprlemmu  8029  suplocexprlemdisj  8031  ltsrprg  8058  mulgt0sr  8089  elreal2  8141  ltresr  8150  ltresr2  8151  axprecex  8191  axpre-ltadd  8197  axpre-mulgt0  8198  axpre-mulext  8199  axpre-suploclemres  8212  subcan2  8494  negcon1  8521  negcon2  8522  lt0neg1  8738  lt0neg2  8739  le0neg1  8740  le0neg2  8741  reapirr  8847  reapmul1  8865  reapneg  8867  remulext1  8869  apti  8892  negap0  8900  divmulap2  8946  reclt1  9166  recgt1  9167  suprleubex  9224  addltmul  9471  elznn0  9588  zapne  9648  zltlen  9652  nn0lt10b  9654  nn0lt2  9655  eluz1  9853  raluz  9906  rexuz  9908  qltlen  9968  cnref1o  9979  rpnegap  10015  ltxr  10104  xlt0neg1  10167  xlt0neg2  10168  xle0neg1  10169  xle0neg2  10170  elixx1  10226  elixx3g  10230  elioo2  10250  icc0r  10255  elicc4  10269  elioopnf  10296  elioomnf  10297  iooneg  10317  iccneg  10318  iccshftr  10323  iccshftl  10325  iccdil  10327  icccntr  10329  iccf1o  10334  elfz1  10343  0fz1  10375  fzpr  10407  fzdifsuc  10411  uzsplit  10422  elfzm1b  10428  elfzp12  10429  fznn0  10443  exfzdc  10582  zsupcllemstep  10585  flqeqceilz  10676  zmodid2  10710  expap0  10927  qsqeqor  11008  bernneq  11018  hasheqf1o  11143  ssenneg  11197  hashfibclem  11199  hashfacen  11201  ccatrn  11290  pfxsuffeqwrdeq  11383  wrd2ind  11408  sqrtmsq2i  11813  maxclpr  11900  minmax  11908  xrmaxlesup  11937  xrnegiso  11940  xrnegcon1d  11942  xrminmax  11943  clim0  11963  climrecvg1n  12026  summodc  12062  fsumsplit  12086  mertenslem2  12215  prodmodc  12257  fprodsplitdc  12275  fprod2dlemstep  12301  dvdsval2  12469  odd2np1lem  12551  even2n  12553  divalgb  12604  divalgmod  12606  bitsval  12622  bitsmod  12635  gcddvds  12652  bezoutlemmain  12687  nnwofdc  12727  isprm3  12808  prmind2  12810  dvdsprime  12812  coprm  12834  prmdvdsexp  12838  sqrt2irr  12852  sqpweven  12865  2sqpwodd  12866  pythagtriplem2  12957  pythagtrip  12974  pceu  12986  pc11  13022  elrest  13448  grpsubeq0  13788  grpsubadd  13790  issubg3  13898  isnsg  13908  eqger  13930  eqglact  13931  eqgid  13932  srgfcl  14106  dvdsrtr  14235  dvdsr02  14239  isunitd  14240  isrhm  14292  isrim0  14295  subsubrng2  14349  subsubrg2  14380  issubrg3  14381  opprdomnbg  14409  2idlelb  14640  mplelbascoe  14834  istopon  14865  isbasis2g  14897  isbasis3g  14898  tgss2  14931  bastop1  14935  iscld  14955  ntreq0  14984  restsn  15032  restopn2  15035  lmbr  15065  cnptoprest2  15092  txbas  15110  eltx  15111  txlm  15131  ishmeo  15156  hmeoimaf1o  15166  ispsmet  15175  ismet  15196  isxmet  15197  ismet2  15206  metn0  15230  elblps  15242  elbl  15243  bdbl  15355  qtopbasss  15373  elcncf  15425  ellimc3apf  15512  elply  15586  sincosq1sgn  15678  sincosq2sgn  15679  cos11  15705  logrpap0b  15728  lgsdir2lem4  15891  gausslemma2dlem0i  15917  lgsquadlem2  15938  m1lgs  15945  2lgsoddprmlem3  15971  2sqlem6  15980  2sqlem9  15984  2sqlem10  15985  vtxdfifiun  16279  wlkl1loop  16340  wlkv0  16351  wlklenvclwlk  16355  upgr2wlkdc  16359  isclwwlk  16376  isclwwlkng  16388  isclwwlknx  16398  clwwlkn2  16403  eupth2lem2dc  16441  eupth2lem3lem6fi  16453  pw1map  16756  subctctexmid  16761  iooref1o  16805  iswomni0  16823