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  888  pm5.75  962  xordidc  1399  19.17  1556  alexdc  1619  nf4dc  1670  abeq2d  2290  cbvralf  2696  cbvrexf  2697  cbvreu  2701  cbvrab  2735  ceqsralt  2764  ralab2  2901  rexab2  2903  euxfr2dc  2922  reu7  2932  reu8  2933  cbvralcsf  3119  cbvrexcsf  3120  cbvreucsf  3121  cbvrabcsf  3122  ralss  3221  rexss  3222  prssg  3749  2ralunsn  3798  eluniab  3821  elintab  3855  dfiun2g  3918  dfiin2g  3919  cbvopab1  4076  cbvmpt  4098  axsep2  4122  bnd2  4173  opeqsn  4252  reusv3  4460  tfisi  4586  opeliunxp  4681  eliunxp  4766  relop  4777  eldm2g  4823  reldm0  4845  relrn0  4889  restidsing  4963  xpmlem  5049  elxp5  5117  cnvpom  5171  cbviota  5183  iota1  5192  sniota  5207  fncnv  5282  fnres  5332  brprcneu  5508  fnopfvb  5557  fvelrnb  5563  fvelimab  5572  fvopab3g  5589  eqfnfv3  5615  eqfnfv2f  5617  fvreseq  5619  fnreseql  5626  rexsupp  5640  respreima  5644  rexrn  5653  ralrn  5654  f1ompt  5667  fsn  5688  fconstfvm  5734  fconst3m  5735  fconst4m  5736  foima2  5752  rexima  5755  ralima  5756  dff13  5768  foeqcnvco  5790  fliftfun  5796  isocnv  5811  isoini  5818  f1oiso  5826  cbvriota  5840  eusvobj2  5860  oprabid  5906  eloprabga  5961  resoprab  5970  eqfnov  5980  eqfnov2  5981  ov6g  6011  funimassov  6023  ovelimab  6024  caovord2  6046  releldm2  6185  dfoprab4  6192  xporderlem  6231  poxp  6232  f1od2  6235  mpoxopovel  6241  brtpos2  6251  brtpos0  6252  rntpos  6257  dftpos3  6262  tpostpos  6264  tpossym  6276  tposoprab  6280  tfrcllemres  6362  frecabcl  6399  frecsuclem  6406  erth2  6579  qliftfun  6616  erovlem  6626  ecopovsym  6630  ecopovsymg  6633  th3qlem1  6636  mapdm0  6662  elpmg  6663  elpm2g  6664  map0e  6685  dom2lem  6771  mapsnen  6810  xpdom2  6830  xpf1o  6843  mapen  6845  ssfilem  6874  diffitest  6886  ac6sfi  6897  ss1o0el1o  6911  isoti  7005  cnvti  7017  omp1eomlem  7092  ismkvnex  7152  nninfwlporlemd  7169  netap  7252  2omotaplemap  7255  ltexpi  7335  ordpipqqs  7372  ltexnqq  7406  enq0enq  7429  enq0sym  7430  enq0tr  7432  nqnq0pi  7436  genipv  7507  genprndl  7519  genprndu  7520  genpdisj  7521  genpassl  7522  genpassu  7523  addcomprg  7576  mulcomprg  7578  ltnqpr  7591  ltnqpri  7592  ltexprlemm  7598  ltexprlemdisj  7604  suplocexprlemmu  7716  suplocexprlemdisj  7718  ltsrprg  7745  mulgt0sr  7776  elreal2  7828  ltresr  7837  ltresr2  7838  axprecex  7878  axpre-ltadd  7884  axpre-mulgt0  7885  axpre-mulext  7886  axpre-suploclemres  7899  subcan2  8181  negcon1  8208  negcon2  8209  lt0neg1  8424  lt0neg2  8425  le0neg1  8426  le0neg2  8427  reapirr  8533  reapmul1  8551  reapneg  8553  remulext1  8555  apti  8578  negap0  8586  divmulap2  8632  reclt1  8852  recgt1  8853  suprleubex  8910  addltmul  9154  elznn0  9267  zapne  9326  zltlen  9330  nn0lt10b  9332  nn0lt2  9333  eluz1  9531  raluz  9577  rexuz  9579  qltlen  9639  cnref1o  9649  rpnegap  9685  ltxr  9774  xlt0neg1  9837  xlt0neg2  9838  xle0neg1  9839  xle0neg2  9840  elixx1  9896  elixx3g  9900  elioo2  9920  icc0r  9925  elicc4  9939  elioopnf  9966  elioomnf  9967  iooneg  9987  iccneg  9988  iccshftr  9993  iccshftl  9995  iccdil  9997  icccntr  9999  iccf1o  10003  elfz1  10012  0fz1  10044  fzpr  10076  fzdifsuc  10080  uzsplit  10091  elfzm1b  10097  elfzp12  10098  fznn0  10112  exfzdc  10239  flqeqceilz  10317  zmodid2  10351  expap0  10549  qsqeqor  10630  bernneq  10640  hasheqf1o  10764  hashfacen  10815  sqrtmsq2i  11143  maxclpr  11230  minmax  11237  xrmaxlesup  11266  xrnegiso  11269  xrnegcon1d  11271  xrminmax  11272  clim0  11292  climrecvg1n  11355  summodc  11390  fsumsplit  11414  mertenslem2  11543  prodmodc  11585  fprodsplitdc  11603  fprod2dlemstep  11629  dvdsval2  11796  odd2np1lem  11876  even2n  11878  divalgb  11929  divalgmod  11931  zsupcllemstep  11945  gcddvds  11963  bezoutlemmain  11998  nnwofdc  12038  isprm3  12117  prmind2  12119  dvdsprime  12121  coprm  12143  prmdvdsexp  12147  sqrt2irr  12161  sqpweven  12174  2sqpwodd  12175  pythagtriplem2  12265  pythagtrip  12282  pceu  12294  pc11  12329  elrest  12694  grpsubeq0  12955  grpsubadd  12957  issubg3  13050  isnsg  13060  eqger  13081  eqglact  13082  eqgid  13083  srgfcl  13154  dvdsrtr  13268  dvdsr02  13272  isunitd  13273  subsubrg2  13365  issubrg3  13366  istopon  13483  isbasis2g  13515  isbasis3g  13516  tgss2  13549  bastop1  13553  iscld  13573  ntreq0  13602  restsn  13650  restopn2  13653  lmbr  13683  cnptoprest2  13710  txbas  13728  eltx  13729  txlm  13749  ishmeo  13774  hmeoimaf1o  13784  ispsmet  13793  ismet  13814  isxmet  13815  ismet2  13824  metn0  13848  elblps  13860  elbl  13861  bdbl  13973  qtopbasss  13991  elcncf  14030  ellimc3apf  14099  sincosq1sgn  14217  sincosq2sgn  14218  cos11  14244  logrpap0b  14267  lgsdir2lem4  14402  m1lgs  14422  2lgsoddprmlem3  14429  2sqlem6  14437  2sqlem9  14441  2sqlem10  14442  subctctexmid  14720  iooref1o  14752  iswomni0  14769