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  893  pm5.75  968  xordidc  1441  19.17  1602  alexdc  1665  nf4dc  1716  abeq2d  2342  cbvralf  2756  cbvrexf  2757  cbvreu  2763  cbvrab  2797  ceqsralt  2827  ralab2  2967  rexab2  2969  euxfr2dc  2988  reu7  2998  reu8  2999  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  ralss  3290  rexss  3291  elif  3614  prssg  3825  2ralunsn  3877  eluniab  3900  elintab  3934  dfiun2g  3997  dfiin2g  3998  cbvopab1  4157  cbvmpt  4179  axsep2  4203  bnd2  4258  opeqsn  4340  reusv3  4552  tfisi  4680  opeliunxp  4776  eliunxp  4864  relop  4875  eldm2g  4922  reldm0  4944  relrn0  4989  restidsing  5064  xpmlem  5152  elxp5  5220  cnvpom  5274  cbviota  5286  iota1  5296  sniota  5312  fncnv  5390  fnres  5443  brprcneu  5625  fnopfvb  5678  fvelrnb  5686  fvelimab  5695  fvopab3g  5712  eqfnfv3  5739  eqfnfv2f  5741  fvreseq  5743  fnreseql  5750  rexsupp  5764  respreima  5768  rexrn  5777  ralrn  5778  f1ompt  5791  fsn  5812  fconstfvm  5864  fconst3m  5865  fconst4m  5866  foima2  5884  rexima  5887  ralima  5888  dff13  5901  foeqcnvco  5923  fliftfun  5929  isocnv  5944  isoini  5951  f1oiso  5959  cbvriota  5975  riotaeqimp  5988  eusvobj2  5996  oprabid  6042  eloprabga  6100  resoprab  6109  eqfnov  6120  eqfnov2  6121  ov6g  6152  funimassov  6164  ovelimab  6165  caovord2  6187  uchoice  6292  releldm2  6340  dfoprab4  6347  xporderlem  6388  poxp  6389  f1od2  6392  mpoxopovel  6398  brtpos2  6408  brtpos0  6409  rntpos  6414  dftpos3  6419  tpostpos  6421  tpossym  6433  tposoprab  6437  tfrcllemres  6519  frecabcl  6556  frecsuclem  6563  erth2  6740  qliftfun  6777  erovlem  6787  ecopovsym  6791  ecopovsymg  6794  th3qlem1  6797  mapdm0  6823  elpmg  6824  elpm2g  6825  map0e  6846  dom2lem  6936  mapsnen  6977  xpdom2  7003  xpf1o  7018  mapen  7020  ssfilem  7050  diffitest  7062  ac6sfi  7073  eqsndc  7081  ss1o0el1o  7091  isoti  7190  cnvti  7202  omp1eomlem  7277  ismkvnex  7338  nninfwlporlemd  7355  en2prde  7382  netap  7456  2omotaplemap  7459  ltexpi  7540  ordpipqqs  7577  ltexnqq  7611  enq0enq  7634  enq0sym  7635  enq0tr  7637  nqnq0pi  7641  genipv  7712  genprndl  7724  genprndu  7725  genpdisj  7726  genpassl  7727  genpassu  7728  addcomprg  7781  mulcomprg  7783  ltnqpr  7796  ltnqpri  7797  ltexprlemm  7803  ltexprlemdisj  7809  suplocexprlemmu  7921  suplocexprlemdisj  7923  ltsrprg  7950  mulgt0sr  7981  elreal2  8033  ltresr  8042  ltresr2  8043  axprecex  8083  axpre-ltadd  8089  axpre-mulgt0  8090  axpre-mulext  8091  axpre-suploclemres  8104  subcan2  8387  negcon1  8414  negcon2  8415  lt0neg1  8631  lt0neg2  8632  le0neg1  8633  le0neg2  8634  reapirr  8740  reapmul1  8758  reapneg  8760  remulext1  8762  apti  8785  negap0  8793  divmulap2  8839  reclt1  9059  recgt1  9060  suprleubex  9117  addltmul  9364  elznn0  9477  zapne  9537  zltlen  9541  nn0lt10b  9543  nn0lt2  9544  eluz1  9742  raluz  9790  rexuz  9792  qltlen  9852  cnref1o  9863  rpnegap  9899  ltxr  9988  xlt0neg1  10051  xlt0neg2  10052  xle0neg1  10053  xle0neg2  10054  elixx1  10110  elixx3g  10114  elioo2  10134  icc0r  10139  elicc4  10153  elioopnf  10180  elioomnf  10181  iooneg  10201  iccneg  10202  iccshftr  10207  iccshftl  10209  iccdil  10211  icccntr  10213  iccf1o  10217  elfz1  10226  0fz1  10258  fzpr  10290  fzdifsuc  10294  uzsplit  10305  elfzm1b  10311  elfzp12  10312  fznn0  10326  exfzdc  10463  zsupcllemstep  10466  flqeqceilz  10557  zmodid2  10591  expap0  10808  qsqeqor  10889  bernneq  10899  hasheqf1o  11024  hashfacen  11076  ccatrn  11162  pfxsuffeqwrdeq  11251  wrd2ind  11276  sqrtmsq2i  11667  maxclpr  11754  minmax  11762  xrmaxlesup  11791  xrnegiso  11794  xrnegcon1d  11796  xrminmax  11797  clim0  11817  climrecvg1n  11880  summodc  11915  fsumsplit  11939  mertenslem2  12068  prodmodc  12110  fprodsplitdc  12128  fprod2dlemstep  12154  dvdsval2  12322  odd2np1lem  12404  even2n  12406  divalgb  12457  divalgmod  12459  bitsval  12475  bitsmod  12488  gcddvds  12505  bezoutlemmain  12540  nnwofdc  12580  isprm3  12661  prmind2  12663  dvdsprime  12665  coprm  12687  prmdvdsexp  12691  sqrt2irr  12705  sqpweven  12718  2sqpwodd  12719  pythagtriplem2  12810  pythagtrip  12827  pceu  12839  pc11  12875  elrest  13300  grpsubeq0  13640  grpsubadd  13642  issubg3  13750  isnsg  13760  eqger  13782  eqglact  13783  eqgid  13784  srgfcl  13957  dvdsrtr  14086  dvdsr02  14090  isunitd  14091  isrhm  14143  isrim0  14146  subsubrng2  14200  subsubrg2  14231  issubrg3  14232  opprdomnbg  14259  2idlelb  14490  mplelbascoe  14677  istopon  14708  isbasis2g  14740  isbasis3g  14741  tgss2  14774  bastop1  14778  iscld  14798  ntreq0  14827  restsn  14875  restopn2  14878  lmbr  14908  cnptoprest2  14935  txbas  14953  eltx  14954  txlm  14974  ishmeo  14999  hmeoimaf1o  15009  ispsmet  15018  ismet  15039  isxmet  15040  ismet2  15049  metn0  15073  elblps  15085  elbl  15086  bdbl  15198  qtopbasss  15216  elcncf  15268  ellimc3apf  15355  elply  15429  sincosq1sgn  15521  sincosq2sgn  15522  cos11  15548  logrpap0b  15571  lgsdir2lem4  15731  gausslemma2dlem0i  15757  lgsquadlem2  15778  m1lgs  15785  2lgsoddprmlem3  15811  2sqlem6  15820  2sqlem9  15824  2sqlem10  15825  vtxdfifiun  16083  wlkl1loop  16130  wlkv0  16141  wlklenvclwlk  16145  upgr2wlkdc  16147  isclwwlk  16163  isclwwlkng  16175  isclwwlknx  16184  clwwlkn2  16189  2omap  16472  pw1map  16474  subctctexmid  16479  iooref1o  16516  iswomni0  16533