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  895  pm5.75  970  xordidc  1443  19.17  1604  alexdc  1667  nf4dc  1718  abeq2d  2344  cbvralf  2758  cbvrexf  2759  cbvreu  2765  cbvrab  2800  ceqsralt  2830  ralab2  2970  rexab2  2972  euxfr2dc  2991  reu7  3001  reu8  3002  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  ralss  3293  rexss  3294  elif  3617  prssg  3830  2ralunsn  3882  eluniab  3905  elintab  3939  dfiun2g  4002  dfiin2g  4003  cbvopab1  4162  cbvmpt  4184  axsep2  4208  bnd2  4263  opeqsn  4345  reusv3  4557  tfisi  4685  opeliunxp  4781  eliunxp  4869  relop  4880  eldm2g  4927  reldm0  4949  relrn0  4994  restidsing  5069  xpmlem  5157  elxp5  5225  cnvpom  5279  cbviota  5291  iota1  5301  sniota  5317  fncnv  5396  fnres  5449  brprcneu  5632  fnopfvb  5685  fvelrnb  5693  fvelimab  5702  fvopab3g  5719  eqfnfv3  5746  eqfnfv2f  5748  fvreseq  5750  fnreseql  5757  rexsupp  5771  respreima  5775  rexrn  5784  ralrn  5785  f1ompt  5798  fsn  5819  fconstfvm  5872  fconst3m  5873  fconst4m  5874  foima2  5892  rexima  5895  ralima  5896  dff13  5909  foeqcnvco  5931  fliftfun  5937  isocnv  5952  isoini  5959  f1oiso  5967  cbvriota  5983  riotaeqimp  5996  eusvobj2  6004  oprabid  6050  eloprabga  6108  resoprab  6117  eqfnov  6128  eqfnov2  6129  ov6g  6160  funimassov  6172  ovelimab  6173  caovord2  6195  uchoice  6300  releldm2  6348  dfoprab4  6355  xporderlem  6396  poxp  6397  f1od2  6400  mpoxopovel  6407  brtpos2  6417  brtpos0  6418  rntpos  6423  dftpos3  6428  tpostpos  6430  tpossym  6442  tposoprab  6446  tfrcllemres  6528  frecabcl  6565  frecsuclem  6572  erth2  6749  qliftfun  6786  erovlem  6796  ecopovsym  6800  ecopovsymg  6803  th3qlem1  6806  mapdm0  6832  elpmg  6833  elpm2g  6834  map0e  6855  dom2lem  6945  mapsnen  6986  xpdom2  7015  xpf1o  7030  mapen  7032  ssfilem  7062  ssfilemd  7064  diffitest  7076  ac6sfi  7087  eqsndc  7095  ss1o0el1o  7105  isoti  7206  cnvti  7218  omp1eomlem  7293  ismkvnex  7354  nninfwlporlemd  7371  en2prde  7398  netap  7473  2omotaplemap  7476  ltexpi  7557  ordpipqqs  7594  ltexnqq  7628  enq0enq  7651  enq0sym  7652  enq0tr  7654  nqnq0pi  7658  genipv  7729  genprndl  7741  genprndu  7742  genpdisj  7743  genpassl  7744  genpassu  7745  addcomprg  7798  mulcomprg  7800  ltnqpr  7813  ltnqpri  7814  ltexprlemm  7820  ltexprlemdisj  7826  suplocexprlemmu  7938  suplocexprlemdisj  7940  ltsrprg  7967  mulgt0sr  7998  elreal2  8050  ltresr  8059  ltresr2  8060  axprecex  8100  axpre-ltadd  8106  axpre-mulgt0  8107  axpre-mulext  8108  axpre-suploclemres  8121  subcan2  8404  negcon1  8431  negcon2  8432  lt0neg1  8648  lt0neg2  8649  le0neg1  8650  le0neg2  8651  reapirr  8757  reapmul1  8775  reapneg  8777  remulext1  8779  apti  8802  negap0  8810  divmulap2  8856  reclt1  9076  recgt1  9077  suprleubex  9134  addltmul  9381  elznn0  9494  zapne  9554  zltlen  9558  nn0lt10b  9560  nn0lt2  9561  eluz1  9759  raluz  9812  rexuz  9814  qltlen  9874  cnref1o  9885  rpnegap  9921  ltxr  10010  xlt0neg1  10073  xlt0neg2  10074  xle0neg1  10075  xle0neg2  10076  elixx1  10132  elixx3g  10136  elioo2  10156  icc0r  10161  elicc4  10175  elioopnf  10202  elioomnf  10203  iooneg  10223  iccneg  10224  iccshftr  10229  iccshftl  10231  iccdil  10233  icccntr  10235  iccf1o  10239  elfz1  10248  0fz1  10280  fzpr  10312  fzdifsuc  10316  uzsplit  10327  elfzm1b  10333  elfzp12  10334  fznn0  10348  exfzdc  10487  zsupcllemstep  10490  flqeqceilz  10581  zmodid2  10615  expap0  10832  qsqeqor  10913  bernneq  10923  hasheqf1o  11048  hashfacen  11101  ccatrn  11187  pfxsuffeqwrdeq  11280  wrd2ind  11305  sqrtmsq2i  11697  maxclpr  11784  minmax  11792  xrmaxlesup  11821  xrnegiso  11824  xrnegcon1d  11826  xrminmax  11827  clim0  11847  climrecvg1n  11910  summodc  11946  fsumsplit  11970  mertenslem2  12099  prodmodc  12141  fprodsplitdc  12159  fprod2dlemstep  12185  dvdsval2  12353  odd2np1lem  12435  even2n  12437  divalgb  12488  divalgmod  12490  bitsval  12506  bitsmod  12519  gcddvds  12536  bezoutlemmain  12571  nnwofdc  12611  isprm3  12692  prmind2  12694  dvdsprime  12696  coprm  12718  prmdvdsexp  12722  sqrt2irr  12736  sqpweven  12749  2sqpwodd  12750  pythagtriplem2  12841  pythagtrip  12858  pceu  12870  pc11  12906  elrest  13331  grpsubeq0  13671  grpsubadd  13673  issubg3  13781  isnsg  13791  eqger  13813  eqglact  13814  eqgid  13815  srgfcl  13989  dvdsrtr  14118  dvdsr02  14122  isunitd  14123  isrhm  14175  isrim0  14178  subsubrng2  14232  subsubrg2  14263  issubrg3  14264  opprdomnbg  14291  2idlelb  14522  mplelbascoe  14709  istopon  14740  isbasis2g  14772  isbasis3g  14773  tgss2  14806  bastop1  14810  iscld  14830  ntreq0  14859  restsn  14907  restopn2  14910  lmbr  14940  cnptoprest2  14967  txbas  14985  eltx  14986  txlm  15006  ishmeo  15031  hmeoimaf1o  15041  ispsmet  15050  ismet  15071  isxmet  15072  ismet2  15081  metn0  15105  elblps  15117  elbl  15118  bdbl  15230  qtopbasss  15248  elcncf  15300  ellimc3apf  15387  elply  15461  sincosq1sgn  15553  sincosq2sgn  15554  cos11  15580  logrpap0b  15603  lgsdir2lem4  15763  gausslemma2dlem0i  15789  lgsquadlem2  15810  m1lgs  15817  2lgsoddprmlem3  15843  2sqlem6  15852  2sqlem9  15856  2sqlem10  15857  vtxdfifiun  16151  wlkl1loop  16212  wlkv0  16223  wlklenvclwlk  16227  upgr2wlkdc  16231  isclwwlk  16248  isclwwlkng  16260  isclwwlknx  16270  clwwlkn2  16275  eupth2lem2dc  16313  eupth2lem3lem6fi  16325  2omap  16615  pw1map  16617  subctctexmid  16622  iooref1o  16659  iswomni0  16676