Theorem sylan2 346

Description: A syllogism inference.

Hypotheses

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

Assertion

Ref	Expression
sylan2	|- ((ph /\ th) -> ch)

Proof of Theorem sylan2

Step	Hyp	Ref	Expression
1		sylan.1	. . . 4 |- ((ph /\ ps) -> ch)
2	1	exp 291	. . 3 |- (ph -> (ps -> ch))
3		sylan2.2	. . 3 |- (th -> ps)
4	2, 3	syl5 22	. 2 |- (ph -> (th -> ch))
5	4	imp 277	1 |- ((ph /\ th) -> ch)

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  sylan2b 347  sylan2br 348  syl2an 349  ssiun 2018  po3nr 2136  dfwe2 2187  trssord 2216  ordelssne 2225  onint 2261  onint0 2262  onnmin 2270  onsssuc 2311  onsucmin 2323  ordsucun 2333  peano5 2394  findsg 2398  tfindsg 2402  tfindsg2 2403  fnbr 2726  funbrfv 2852  cleqfv 2880  isofrlem 2939  tfrlem8 2956  tfrlem9 2957  tfrlem10 2958  tfrlem11 2959  tfr3 2964  oasuc 3131  omsuc 3133  oalim 3135  omlim 3136  oalimcl 3162  oaass 3163  nndi 3180  nnmordi 3188  nnaordex 3191  nnawordex 3192  ecoprass 3256  ecoprdi 3257  domentr 3326  undom 3342  sbthlem9 3357  mapunen 3397  ssenen 3399  phplem4 3406  phplem5 3407  php 3409  php3 3411  onomeneq 3414  omsucdom 3418  ssfi 3430  unbnn2 3436  unfi 3441  omex 3475  aceq3 3556  aceq5 3563  aceq6b 3565  ac5b 3574  zornlem3 3605  imadomg 3616  sucdom 3648  unxpdomlem 3649  ondomon 3662  alephnbtwn 3674  alephordi 3679  cfom 3710  axrepndlem2 3739  axpowndlem4 3746  axinfndlem1 3751  axacndlem5 3757  addclpi 3814  addasspi 3817  mulasspi 3819  distrpi 3820  mulcanpi 3821  indpi 3828  ltapq 3870  ltrpq 3879  prcdpq 3891  genpass 3906  distrlem1pr 3921  distrlem2pr 3922  distrlem4pr 3924  psslinpr 3929  prlem934b 3932  ltaddpr 3934  ltexprlem6 3941  ltexprlem7 3942  prlem936b 3948  prlem936 3949  reclem3pr 3952  reclem4pr 3953  1idsr 4001  recexsrlem 4006  addgt0sr 4007  suppsr3 4018  axrecex 4079  axsup 4088  subneg2t 4158  resubclt 4173  mulneg2t 4197  negdi2t 4201  subsubt 4203  div23t 4240  divnegt 4259  recdivt 4270  le2tri3 4311  ltaddsubt 4357  nndiv 4453  sup2 4510  nnunb 4520  arch 4521  nn0ge0t 4550  nn0addclt 4551  nn0leltp1t 4557  zaddclt 4590  zsubclt 4591  zrevaddclt 4592  elnn0nn 4593  zltp1let 4597  zleltp1t 4598  peano2uz 4602  uzind 4603  uzwo 4605  nnwoOLD 4608  uzwo3lem1 4614  zmax 4618  zbtwnre 4619  rebtwnz 4620  flgzt 4626  qaddclt 4642  qsubclt 4645  qrecclt 4646  qdivclt 4647  qrevaddclt 4648  qbtwnre 4650  seqrn 4673  expp1t 4678  replimt 4798  facclt 4874  ruclem13 4897  znnenlem 4929  infxpidmlem1 4933  infxpidmlem8 4940  infxpidmlem11 4943  infxpidmlem12 4944  infdif 4948  hvsubclt 4998  hvsubcan1t 5016  his5 5050  his7 5051  hlimcaui 5141  shorth 5176  pjvalt 5246  pjoml 5271  shscl 5282  chsscon2t 5419  chpsscon2t 5422  chdmm3t 5440  chdmm4t 5441  chdmj3t 5444  chdmj4t 5445  spansnmul 5469  spansnsclt 5541  spansncv 5542  5oalem4 5547  pjadjco 5631  pjnormss 5638  pjclem4 5653  pjadj2co 5656  pj3s 5659  pj3 5660  spansncv2t 5725  dmdbr 5731  atcveq0 5746  chcv1t 5751  chcv2t 5752  cvexchlem 5759  cvp 5764  atcv1 5768  atexch 5769  atcvatlem 5770  mdsymlem3 5778  mdsymlem5 5780  sumdmdlem 5786

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org