Theorem sylan2b 285

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 119	. 2 |- ( ph -> ch )
3		sylan2b.2	. 2 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylan2 284	1 |- ( ( ps /\ ph ) -> th )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl2anb  289  dcor  925  bm1.1  2150  eqtr3  2185  elnelne1  2439  elnelne2  2440  morex  2909  reuss2  3401  reupick  3405  rabsneu  3648  opabss  4045  triun  4092  poirr  4284  wepo  4336  wetrep  4337  rexxfrd  4440  reg3exmidlemwe  4555  nnsuc  4592  fnfco  5361  fun11iun  5452  fnressn  5670  fvpr1g  5690  fvtp1g  5692  fvtp3g  5694  fvtp3  5697  f1mpt  5738  caovlem2d  6030  offval  6056  dfoprab3  6156  1stconst  6185  2ndconst  6186  poxp  6196  tfrlemisucaccv  6289  tfr1onlemsucaccv  6305  tfrcllemsucaccv  6318  fiintim  6890  addclpi  7264  addnidpig  7273  reapmul1  8489  nnnn0addcl  9140  un0addcl  9143  un0mulcl  9144  zltnle  9233  nn0ge0div  9274  uzind3  9300  uzind4  9522  ltsubrp  9622  ltaddrp  9623  xrlttr  9727  xrltso  9728  xltnegi  9767  xaddnemnf  9789  xaddnepnf  9790  xaddcom  9793  xnegdi  9800  xsubge0  9813  fzind2  10170  qltnle  10177  qbtwnxr  10189  exp3vallem  10452  expp1  10458  expnegap0  10459  expcllem  10462  mulexpzap  10491  expaddzap  10495  expmulzap  10497  hashunlem  10713  shftf  10768  sqrtdiv  10980  mulcn2  11249  summodclem2  11319  fsum3  11324  cvgratz  11469  prodmodclem2  11514  zproddc  11516  prodsnf  11529  dvdsflip  11785  dvdsfac  11794  lcmgcdlem  12005  rpexp1i  12082  hashdvds  12149  hashgcdlem  12166  phisum  12168  pcqcl  12234  pcid  12251  ssnnctlemct  12375  lmss  12846  xmetrtri  12976  blssioo  13145  divcnap  13155  dedekindicc  13211  dvidlemap  13260  dvrecap  13277  dveflem  13287  lgsval3  13519  lgsdir2  13534  2sqlem6  13556  bj-bdfindes  13791  bj-findes  13823