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  2924  rexab2  2926  euxfr2dc  2945  reu7  2955  reu8  2956  cbvralcsf  3143  cbvrexcsf  3144  cbvreucsf  3145  cbvrabcsf  3146  ralss  3245  rexss  3246  prssg  3775  2ralunsn  3824  eluniab  3847  elintab  3881  dfiun2g  3944  dfiin2g  3945  cbvopab1  4102  cbvmpt  4124  axsep2  4148  bnd2  4202  opeqsn  4281  reusv3  4491  tfisi  4619  opeliunxp  4714  eliunxp  4801  relop  4812  eldm2g  4858  reldm0  4880  relrn0  4924  restidsing  4998  xpmlem  5086  elxp5  5154  cnvpom  5208  cbviota  5220  iota1  5229  sniota  5245  fncnv  5320  fnres  5370  brprcneu  5547  fnopfvb  5598  fvelrnb  5604  fvelimab  5613  fvopab3g  5630  eqfnfv3  5657  eqfnfv2f  5659  fvreseq  5661  fnreseql  5668  rexsupp  5682  respreima  5686  rexrn  5695  ralrn  5696  f1ompt  5709  fsn  5730  fconstfvm  5776  fconst3m  5777  fconst4m  5778  foima2  5794  rexima  5797  ralima  5798  dff13  5811  foeqcnvco  5833  fliftfun  5839  isocnv  5854  isoini  5861  f1oiso  5869  cbvriota  5884  eusvobj2  5904  oprabid  5950  eloprabga  6005  resoprab  6014  eqfnov  6025  eqfnov2  6026  ov6g  6056  funimassov  6068  ovelimab  6069  caovord2  6091  uchoice  6190  releldm2  6238  dfoprab4  6245  xporderlem  6284  poxp  6285  f1od2  6288  mpoxopovel  6294  brtpos2  6304  brtpos0  6305  rntpos  6310  dftpos3  6315  tpostpos  6317  tpossym  6329  tposoprab  6333  tfrcllemres  6415  frecabcl  6452  frecsuclem  6459  erth2  6634  qliftfun  6671  erovlem  6681  ecopovsym  6685  ecopovsymg  6688  th3qlem1  6691  mapdm0  6717  elpmg  6718  elpm2g  6719  map0e  6740  dom2lem  6826  mapsnen  6865  xpdom2  6885  xpf1o  6900  mapen  6902  ssfilem  6931  diffitest  6943  ac6sfi  6954  ss1o0el1o  6969  isoti  7066  cnvti  7078  omp1eomlem  7153  ismkvnex  7214  nninfwlporlemd  7231  netap  7314  2omotaplemap  7317  ltexpi  7397  ordpipqqs  7434  ltexnqq  7468  enq0enq  7491  enq0sym  7492  enq0tr  7494  nqnq0pi  7498  genipv  7569  genprndl  7581  genprndu  7582  genpdisj  7583  genpassl  7584  genpassu  7585  addcomprg  7638  mulcomprg  7640  ltnqpr  7653  ltnqpri  7654  ltexprlemm  7660  ltexprlemdisj  7666  suplocexprlemmu  7778  suplocexprlemdisj  7780  ltsrprg  7807  mulgt0sr  7838  elreal2  7890  ltresr  7899  ltresr2  7900  axprecex  7940  axpre-ltadd  7946  axpre-mulgt0  7947  axpre-mulext  7948  axpre-suploclemres  7961  subcan2  8244  negcon1  8271  negcon2  8272  lt0neg1  8487  lt0neg2  8488  le0neg1  8489  le0neg2  8490  reapirr  8596  reapmul1  8614  reapneg  8616  remulext1  8618  apti  8641  negap0  8649  divmulap2  8695  reclt1  8915  recgt1  8916  suprleubex  8973  addltmul  9219  elznn0  9332  zapne  9391  zltlen  9395  nn0lt10b  9397  nn0lt2  9398  eluz1  9596  raluz  9643  rexuz  9645  qltlen  9705  cnref1o  9716  rpnegap  9752  ltxr  9841  xlt0neg1  9904  xlt0neg2  9905  xle0neg1  9906  xle0neg2  9907  elixx1  9963  elixx3g  9967  elioo2  9987  icc0r  9992  elicc4  10006  elioopnf  10033  elioomnf  10034  iooneg  10054  iccneg  10055  iccshftr  10060  iccshftl  10062  iccdil  10064  icccntr  10066  iccf1o  10070  elfz1  10079  0fz1  10111  fzpr  10143  fzdifsuc  10147  uzsplit  10158  elfzm1b  10164  elfzp12  10165  fznn0  10179  exfzdc  10307  flqeqceilz  10389  zmodid2  10423  expap0  10640  qsqeqor  10721  bernneq  10731  hasheqf1o  10856  hashfacen  10907  sqrtmsq2i  11279  maxclpr  11366  minmax  11373  xrmaxlesup  11402  xrnegiso  11405  xrnegcon1d  11407  xrminmax  11408  clim0  11428  climrecvg1n  11491  summodc  11526  fsumsplit  11550  mertenslem2  11679  prodmodc  11721  fprodsplitdc  11739  fprod2dlemstep  11765  dvdsval2  11933  odd2np1lem  12013  even2n  12015  divalgb  12066  divalgmod  12068  zsupcllemstep  12082  gcddvds  12100  bezoutlemmain  12135  nnwofdc  12175  isprm3  12256  prmind2  12258  dvdsprime  12260  coprm  12282  prmdvdsexp  12286  sqrt2irr  12300  sqpweven  12313  2sqpwodd  12314  pythagtriplem2  12404  pythagtrip  12421  pceu  12433  pc11  12469  elrest  12857  grpsubeq0  13158  grpsubadd  13160  issubg3  13262  isnsg  13272  eqger  13294  eqglact  13295  eqgid  13296  srgfcl  13469  dvdsrtr  13597  dvdsr02  13601  isunitd  13602  isrhm  13654  isrim0  13657  subsubrng2  13711  subsubrg2  13742  issubrg3  13743  opprdomnbg  13770  2idlelb  14001  istopon  14181  isbasis2g  14213  isbasis3g  14214  tgss2  14247  bastop1  14251  iscld  14271  ntreq0  14300  restsn  14348  restopn2  14351  lmbr  14381  cnptoprest2  14408  txbas  14426  eltx  14427  txlm  14447  ishmeo  14472  hmeoimaf1o  14482  ispsmet  14491  ismet  14512  isxmet  14513  ismet2  14522  metn0  14546  elblps  14558  elbl  14559  bdbl  14671  qtopbasss  14689  elcncf  14728  ellimc3apf  14814  elply  14880  sincosq1sgn  14961  sincosq2sgn  14962  cos11  14988  logrpap0b  15011  lgsdir2lem4  15147  gausslemma2dlem0i  15173  m1lgs  15192  2lgsoddprmlem3  15199  2sqlem6  15207  2sqlem9  15211  2sqlem10  15212  subctctexmid  15491  iooref1o  15524  iswomni0  15541