Theorem bitrdi 196

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitrdi.1	|- ( ph -> ( ps <-> ch ) )
bitrdi.2	|- ( ch <-> th )

Assertion

Ref	Expression
bitrdi	|- ( ph -> ( ps <-> th ) )

Proof of Theorem bitrdi

Step	Hyp	Ref	Expression
1		bitrdi.1	. 2 |- ( ph -> ( ps <-> ch ) )
2		bitrdi.2	. . 3 |- ( ch <-> th )
3	2	a1i 9	. 2 |- ( ph -> ( ch <-> th ) )
4	1, 3	bitrd 188	1 |- ( ph -> ( ps <-> th ) )

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  1567  alexdc  1630  nf4dc  1681  abeq2d  2306  cbvralf  2718  cbvrexf  2719  cbvreu  2724  cbvrab  2758  ceqsralt  2787  ralab2  2925  rexab2  2927  euxfr2dc  2946  reu7  2956  reu8  2957  cbvralcsf  3144  cbvrexcsf  3145  cbvreucsf  3146  cbvrabcsf  3147  ralss  3246  rexss  3247  prssg  3776  2ralunsn  3825  eluniab  3848  elintab  3882  dfiun2g  3945  dfiin2g  3946  cbvopab1  4103  cbvmpt  4125  axsep2  4149  bnd2  4203  opeqsn  4282  reusv3  4492  tfisi  4620  opeliunxp  4715  eliunxp  4802  relop  4813  eldm2g  4859  reldm0  4881  relrn0  4925  restidsing  4999  xpmlem  5087  elxp5  5155  cnvpom  5209  cbviota  5221  iota1  5230  sniota  5246  fncnv  5321  fnres  5371  brprcneu  5548  fnopfvb  5599  fvelrnb  5605  fvelimab  5614  fvopab3g  5631  eqfnfv3  5658  eqfnfv2f  5660  fvreseq  5662  fnreseql  5669  rexsupp  5683  respreima  5687  rexrn  5696  ralrn  5697  f1ompt  5710  fsn  5731  fconstfvm  5777  fconst3m  5778  fconst4m  5779  foima2  5795  rexima  5798  ralima  5799  dff13  5812  foeqcnvco  5834  fliftfun  5840  isocnv  5855  isoini  5862  f1oiso  5870  cbvriota  5885  eusvobj2  5905  oprabid  5951  eloprabga  6006  resoprab  6015  eqfnov  6026  eqfnov2  6027  ov6g  6058  funimassov  6070  ovelimab  6071  caovord2  6093  uchoice  6192  releldm2  6240  dfoprab4  6247  xporderlem  6286  poxp  6287  f1od2  6290  mpoxopovel  6296  brtpos2  6306  brtpos0  6307  rntpos  6312  dftpos3  6317  tpostpos  6319  tpossym  6331  tposoprab  6335  tfrcllemres  6417  frecabcl  6454  frecsuclem  6461  erth2  6636  qliftfun  6673  erovlem  6683  ecopovsym  6687  ecopovsymg  6690  th3qlem1  6693  mapdm0  6719  elpmg  6720  elpm2g  6721  map0e  6742  dom2lem  6828  mapsnen  6867  xpdom2  6887  xpf1o  6902  mapen  6904  ssfilem  6933  diffitest  6945  ac6sfi  6956  ss1o0el1o  6971  isoti  7068  cnvti  7080  omp1eomlem  7155  ismkvnex  7216  nninfwlporlemd  7233  netap  7316  2omotaplemap  7319  ltexpi  7399  ordpipqqs  7436  ltexnqq  7470  enq0enq  7493  enq0sym  7494  enq0tr  7496  nqnq0pi  7500  genipv  7571  genprndl  7583  genprndu  7584  genpdisj  7585  genpassl  7586  genpassu  7587  addcomprg  7640  mulcomprg  7642  ltnqpr  7655  ltnqpri  7656  ltexprlemm  7662  ltexprlemdisj  7668  suplocexprlemmu  7780  suplocexprlemdisj  7782  ltsrprg  7809  mulgt0sr  7840  elreal2  7892  ltresr  7901  ltresr2  7902  axprecex  7942  axpre-ltadd  7948  axpre-mulgt0  7949  axpre-mulext  7950  axpre-suploclemres  7963  subcan2  8246  negcon1  8273  negcon2  8274  lt0neg1  8489  lt0neg2  8490  le0neg1  8491  le0neg2  8492  reapirr  8598  reapmul1  8616  reapneg  8618  remulext1  8620  apti  8643  negap0  8651  divmulap2  8697  reclt1  8917  recgt1  8918  suprleubex  8975  addltmul  9222  elznn0  9335  zapne  9394  zltlen  9398  nn0lt10b  9400  nn0lt2  9401  eluz1  9599  raluz  9646  rexuz  9648  qltlen  9708  cnref1o  9719  rpnegap  9755  ltxr  9844  xlt0neg1  9907  xlt0neg2  9908  xle0neg1  9909  xle0neg2  9910  elixx1  9966  elixx3g  9970  elioo2  9990  icc0r  9995  elicc4  10009  elioopnf  10036  elioomnf  10037  iooneg  10057  iccneg  10058  iccshftr  10063  iccshftl  10065  iccdil  10067  icccntr  10069  iccf1o  10073  elfz1  10082  0fz1  10114  fzpr  10146  fzdifsuc  10150  uzsplit  10161  elfzm1b  10167  elfzp12  10168  fznn0  10182  exfzdc  10310  flqeqceilz  10392  zmodid2  10426  expap0  10643  qsqeqor  10724  bernneq  10734  hasheqf1o  10859  hashfacen  10910  sqrtmsq2i  11282  maxclpr  11369  minmax  11376  xrmaxlesup  11405  xrnegiso  11408  xrnegcon1d  11410  xrminmax  11411  clim0  11431  climrecvg1n  11494  summodc  11529  fsumsplit  11553  mertenslem2  11682  prodmodc  11724  fprodsplitdc  11742  fprod2dlemstep  11768  dvdsval2  11936  odd2np1lem  12016  even2n  12018  divalgb  12069  divalgmod  12071  zsupcllemstep  12085  gcddvds  12103  bezoutlemmain  12138  nnwofdc  12178  isprm3  12259  prmind2  12261  dvdsprime  12263  coprm  12285  prmdvdsexp  12289  sqrt2irr  12303  sqpweven  12316  2sqpwodd  12317  pythagtriplem2  12407  pythagtrip  12424  pceu  12436  pc11  12472  elrest  12860  grpsubeq0  13161  grpsubadd  13163  issubg3  13265  isnsg  13275  eqger  13297  eqglact  13298  eqgid  13299  srgfcl  13472  dvdsrtr  13600  dvdsr02  13604  isunitd  13605  isrhm  13657  isrim0  13660  subsubrng2  13714  subsubrg2  13745  issubrg3  13746  opprdomnbg  13773  2idlelb  14004  istopon  14192  isbasis2g  14224  isbasis3g  14225  tgss2  14258  bastop1  14262  iscld  14282  ntreq0  14311  restsn  14359  restopn2  14362  lmbr  14392  cnptoprest2  14419  txbas  14437  eltx  14438  txlm  14458  ishmeo  14483  hmeoimaf1o  14493  ispsmet  14502  ismet  14523  isxmet  14524  ismet2  14533  metn0  14557  elblps  14569  elbl  14570  bdbl  14682  qtopbasss  14700  elcncf  14752  ellimc3apf  14839  elply  14913  sincosq1sgn  15002  sincosq2sgn  15003  cos11  15029  logrpap0b  15052  lgsdir2lem4  15188  gausslemma2dlem0i  15214  lgsquadlem2  15235  m1lgs  15242  2lgsoddprmlem3  15268  2sqlem6  15277  2sqlem9  15281  2sqlem10  15282  subctctexmid  15561  iooref1o  15594  iswomni0  15611