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  935  bm1.1  2162  eqtr3  2197  elnelne1  2451  elnelne2  2452  morex  2922  reuss2  3416  reupick  3420  rabsneu  3666  opabss  4068  triun  4115  poirr  4308  wepo  4360  wetrep  4361  rexxfrd  4464  reg3exmidlemwe  4579  nnsuc  4616  fnfco  5391  fun11iun  5483  fnressn  5703  fvpr1g  5723  fvtp1g  5725  fvtp3g  5727  fvtp3  5730  f1mpt  5772  caovlem2d  6067  offval  6090  dfoprab3  6192  1stconst  6222  2ndconst  6223  poxp  6233  tfrlemisucaccv  6326  tfr1onlemsucaccv  6342  tfrcllemsucaccv  6355  fiintim  6928  addclpi  7326  addnidpig  7335  reapmul1  8552  nnnn0addcl  9206  un0addcl  9209  un0mulcl  9210  zltnle  9299  nn0ge0div  9340  uzind3  9366  uzind4  9588  ltsubrp  9690  ltaddrp  9691  xrlttr  9795  xrltso  9796  xltnegi  9835  xaddnemnf  9857  xaddnepnf  9858  xaddcom  9861  xnegdi  9868  xsubge0  9881  fzind2  10239  qltnle  10246  qbtwnxr  10258  exp3vallem  10521  expp1  10527  expnegap0  10528  expcllem  10531  mulexpzap  10560  expaddzap  10564  expmulzap  10566  hashunlem  10784  shftf  10839  sqrtdiv  11051  mulcn2  11320  summodclem2  11390  fsum3  11395  cvgratz  11540  prodmodclem2  11585  zproddc  11587  prodsnf  11600  dvdsflip  11857  dvdsfac  11866  lcmgcdlem  12077  rpexp1i  12154  hashdvds  12221  hashgcdlem  12238  phisum  12240  pcqcl  12306  pcid  12323  ssnnctlemct  12447  issubmd  12865  grpinvnzcl  12942  mulgneg  13001  mulgnn0z  13010  01eq0ring  13330  lmss  13749  xmetrtri  13879  blssioo  14048  divcnap  14058  dedekindicc  14114  dvidlemap  14163  dvrecap  14180  dveflem  14190  lgsval3  14422  lgsdir2  14437  2sqlem6  14470  bj-bdfindes  14704  bj-findes  14736