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  941  bm1.1  2214  eqtr3  2249  elnelne1  2504  elnelne2  2505  morex  2987  reuss2  3484  reupick  3488  rabsneu  3739  invdisjrab  4077  opabss  4148  triun  4195  poirr  4398  wepo  4450  wetrep  4451  rexxfrd  4554  reg3exmidlemwe  4671  nnsuc  4708  fnfco  5502  fun11iun  5595  fnressn  5829  fvpr1g  5849  fvtp1g  5851  fvtp3g  5853  fvtp3  5856  f1mpt  5901  caovlem2d  6204  offval  6232  dfoprab3  6343  1stconst  6373  2ndconst  6374  poxp  6384  tfrlemisucaccv  6477  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  fiintim  7104  pr1or2  7378  addclpi  7525  addnidpig  7534  reapmul1  8753  nnnn0addcl  9410  un0addcl  9413  un0mulcl  9414  zltnle  9503  nn0ge0div  9545  uzind3  9571  uzind4  9795  ltsubrp  9898  ltaddrp  9899  xrlttr  10003  xrltso  10004  xltnegi  10043  xaddnemnf  10065  xaddnepnf  10066  xaddcom  10069  xnegdi  10076  xsubge0  10089  fzind2  10457  qltnle  10475  qbtwnxr  10489  exp3vallem  10774  expp1  10780  expnegap0  10781  expcllem  10784  mulexpzap  10813  expaddzap  10817  expmulzap  10819  hashunlem  11038  cats1un  11268  reuccatpfxs1  11294  shftf  11356  sqrtdiv  11568  mulcn2  11838  summodclem2  11908  fsum3  11913  cvgratz  12058  prodmodclem2  12103  zproddc  12105  prodsnf  12118  dvdsflip  12377  dvdsfac  12386  bitsfzolem  12480  lcmgcdlem  12614  rpexp1i  12691  hashdvds  12758  hashgcdlem  12775  phisum  12778  pcqcl  12844  pcid  12862  ssnnctlemct  13032  issubmd  13522  grpinvnzcl  13620  mulgneg  13692  mulgnn0z  13701  01eq0ring  14168  lmss  14935  xmetrtri  15065  blssioo  15242  divcnap  15254  dedekindicc  15322  dvidlemap  15380  dvidrelem  15381  dvidsslem  15382  dvrecap  15402  dveflem  15415  lgsval3  15712  lgsdir2  15727  2sqlem6  15814  umgredg  15958  umgrpredgv  15960  umgredgne  15963  umgredgnlp  15965  usgredgppren  16010  edgssv2en  16012  uspgredg2vlem  16033  usgredg2vlem1  16035  bj-bdfindes  16367  bj-findes  16399  2omap  16418