Theorem sylan2b 287

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)

Hypotheses

Ref	Expression
sylan2b.1	|- ( ph <-> ch )
sylan2b.2	|- ( ( ps /\ ch ) -> th )

Assertion

Ref	Expression
sylan2b	|- ( ( ps /\ ph ) -> th )

Proof of Theorem sylan2b

Step	Hyp	Ref	Expression
1		sylan2b.1	. . 3 |- ( ph <-> ch )
2	1	biimpi 120	. 2 |- ( ph -> ch )
3		sylan2b.2	. 2 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylan2 286	1 |- ( ( ps /\ ph ) -> th )

Syntax hints:   -> wi 4   /\ wa 104   <-> 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:  syl2anb  291  dcor  937  bm1.1  2178  eqtr3  2213  elnelne1  2468  elnelne2  2469  morex  2944  reuss2  3439  reupick  3443  rabsneu  3691  opabss  4093  triun  4140  poirr  4338  wepo  4390  wetrep  4391  rexxfrd  4494  reg3exmidlemwe  4611  nnsuc  4648  fnfco  5428  fun11iun  5521  fnressn  5744  fvpr1g  5764  fvtp1g  5766  fvtp3g  5768  fvtp3  5771  f1mpt  5814  caovlem2d  6111  offval  6138  dfoprab3  6244  1stconst  6274  2ndconst  6275  poxp  6285  tfrlemisucaccv  6378  tfr1onlemsucaccv  6394  tfrcllemsucaccv  6407  fiintim  6985  addclpi  7387  addnidpig  7396  reapmul1  8614  nnnn0addcl  9270  un0addcl  9273  un0mulcl  9274  zltnle  9363  nn0ge0div  9404  uzind3  9430  uzind4  9653  ltsubrp  9756  ltaddrp  9757  xrlttr  9861  xrltso  9862  xltnegi  9901  xaddnemnf  9923  xaddnepnf  9924  xaddcom  9927  xnegdi  9934  xsubge0  9947  fzind2  10306  qltnle  10313  qbtwnxr  10326  exp3vallem  10611  expp1  10617  expnegap0  10618  expcllem  10621  mulexpzap  10650  expaddzap  10654  expmulzap  10656  hashunlem  10875  shftf  10974  sqrtdiv  11186  mulcn2  11455  summodclem2  11525  fsum3  11530  cvgratz  11675  prodmodclem2  11720  zproddc  11722  prodsnf  11735  dvdsflip  11993  dvdsfac  12002  lcmgcdlem  12215  rpexp1i  12292  hashdvds  12359  hashgcdlem  12376  phisum  12378  pcqcl  12444  pcid  12462  ssnnctlemct  12603  issubmd  13046  grpinvnzcl  13144  mulgneg  13210  mulgnn0z  13219  01eq0ring  13685  lmss  14414  xmetrtri  14544  blssioo  14713  divcnap  14723  dedekindicc  14787  dvidlemap  14845  dvrecap  14862  dveflem  14872  lgsval3  15134  lgsdir2  15149  2sqlem6  15207  bj-bdfindes  15441  bj-findes  15473