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  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  11190  pfxsuffeqwrdeq  11283  wrd2ind  11308  sqrtmsq2i  11713  maxclpr  11800  minmax  11808  xrmaxlesup  11837  xrnegiso  11840  xrnegcon1d  11842  xrminmax  11843  clim0  11863  climrecvg1n  11926  summodc  11962  fsumsplit  11986  mertenslem2  12115  prodmodc  12157  fprodsplitdc  12175  fprod2dlemstep  12201  dvdsval2  12369  odd2np1lem  12451  even2n  12453  divalgb  12504  divalgmod  12506  bitsval  12522  bitsmod  12535  gcddvds  12552  bezoutlemmain  12587  nnwofdc  12627  isprm3  12708  prmind2  12710  dvdsprime  12712  coprm  12734  prmdvdsexp  12738  sqrt2irr  12752  sqpweven  12765  2sqpwodd  12766  pythagtriplem2  12857  pythagtrip  12874  pceu  12886  pc11  12922  elrest  13347  grpsubeq0  13687  grpsubadd  13689  issubg3  13797  isnsg  13807  eqger  13829  eqglact  13830  eqgid  13831  srgfcl  14005  dvdsrtr  14134  dvdsr02  14138  isunitd  14139  isrhm  14191  isrim0  14194  subsubrng2  14248  subsubrg2  14279  issubrg3  14280  opprdomnbg  14307  2idlelb  14538  mplelbascoe  14725  istopon  14756  isbasis2g  14788  isbasis3g  14789  tgss2  14822  bastop1  14826  iscld  14846  ntreq0  14875  restsn  14923  restopn2  14926  lmbr  14956  cnptoprest2  14983  txbas  15001  eltx  15002  txlm  15022  ishmeo  15047  hmeoimaf1o  15057  ispsmet  15066  ismet  15087  isxmet  15088  ismet2  15097  metn0  15121  elblps  15133  elbl  15134  bdbl  15246  qtopbasss  15264  elcncf  15316  ellimc3apf  15403  elply  15477  sincosq1sgn  15569  sincosq2sgn  15570  cos11  15596  logrpap0b  15619  lgsdir2lem4  15779  gausslemma2dlem0i  15805  lgsquadlem2  15826  m1lgs  15833  2lgsoddprmlem3  15859  2sqlem6  15868  2sqlem9  15872  2sqlem10  15873  vtxdfifiun  16167  wlkl1loop  16228  wlkv0  16239  wlklenvclwlk  16243  upgr2wlkdc  16247  isclwwlk  16264  isclwwlkng  16276  isclwwlknx  16286  clwwlkn2  16291  eupth2lem2dc  16329  eupth2lem3lem6fi  16341  2omap  16645  pw1map  16647  subctctexmid  16652  iooref1o  16689  iswomni0  16707