Theorem sylan 343

Description: A syllogism inference.

Hypotheses

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

Assertion

Ref	Expression
sylan	|- ((th /\ ps) -> ch)

Proof of Theorem sylan

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

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  sylanb 344  sylanbr 345  syl2an 349  sylan12 355  syl3an1 619  eupick 1055  vtocl2gf 1385  sonr 2143  sotr 2144  so2nr 2146  so3nr 2147  supsn 2168  wecmpep 2193  wetrep 2194  wefrc 2195  wereu 2197  ordelss 2215  tz7.5 2220  ordelord 2221  onelon 2223  tz7.7 2224  ordin 2228  ordtri3or 2230  ordsssuc 2310  onmindif 2312  ordsucss 2320  ordsucelsuc 2324  ordunisssuc 2334  limsssuc 2362  ordom 2382  limom 2387  nnsuc 2389  imadif 2714  feu 2767  f1oco 2816  ffoss 2820  funbrfv 2852  fvco 2865  fvopabg 2872  fvelrn 2883  ffvrn 2890  fsn2 2896  funfvima 2904  f1ocnvfv1 2919  f1ocnvfv2 2920  isocnv 2934  isotr 2935  isotrALT 2936  isomin 2937  isoini 2938  isowe 2941  f1oiso 2942  iinon 2948  tfrlem2 2950  tfrlem11 2959  rdglimt 2986  tz7.48lem 2993  oesuc 3134  oalimcl 3162  oaass 3163  omordi 3164  oen0 3165  nnmass 3181  nnmordi 3188  nnaordex 3191  nnawordex 3192  ecoprass 3256  mapsn 3269  endomtr 3325  fundmen 3333  pw2en 3348  sdomdomtr 3370  mapenlem1 3384  mapenlem2 3385  mapxpen 3390  xpmapenlem4 3394  mapunen 3397  ssenen 3399  phplem2 3404  omsucdom 3418  sucdomi 3419  ssfi 3430  isfinite2 3437  unfilem1 3438  r1ord 3499  r1val1 3502  rankr1 3518  r1pwcl 3530  karden 3551  ac6lem 3575  ondomon 3662  ondomcard 3663  alephordi 3679  cardaleph 3690  cardinfima 3696  cflim 3704  addclpi 3814  addasspi 3817  mulasspi 3819  addnidpi 3822  ltexpq 3874  prub 3892  genpnnp 3902  genpass 3906  addclprlem1 3912  mulclprlem 3915  1idpr 3927  prlem934b 3932  prlem934 3933  ltexprlem4 3939  ltexprlem6 3941  ltexprlem7 3942  reclem3pr 3952  suplem2pr 3956  00sr 4002  mulgt0sr 4008  recexsr 4010  map2psrpr 4014  suppsr 4016  supsrlem6 4024  supre 4054  adddirt 4103  add4t 4127  mul4t 4177  negdi3t 4202  divasst 4239  divnegt 4259  divadddivt 4264  divdiv23t 4271  le2tri3 4311  ltaddsubt 4357  ltnegcon1t 4367  lenegcon1t 4369  ltdivmult 4408  nnltp1let 4449  nnunb 4520  nn0addclt 4551  elnnz1 4581  zaddclt 4590  zltp1let 4597  zlem1ltt 4599  sqznn 4600  uzind 4603  uzwo 4605  nnwoOLD 4608  btwnz 4613  zmax 4618  zbtwnre 4619  rebtwnz 4620  qaddclt 4642  qrecclt 4646  qdivclt 4647  qbtwnre 4650  seqrn2 4674  expcllem 4682  sqrlem5 4735  clim2 4881  ruclem13 4897  infxpidmlem1 4933  infxpidmlem7 4939  infxpidmlem10 4942  infxpidmlem11 4943  infxpidmlem12 4944  infdif 4948  infmap2lem2 4952  hvadd4t 5013  hvaddsubasst 5018  hlim2 5112  hsn0elch 5155  ocsh 5164  occllem6 5185  projlem21 5213  projlem25 5217  projlem26 5218  pjpjtht 5262  pjopt 5264  pjpot 5265  elspanclt 5306  chsscon1t 5418  chpsscon1t 5421  chdmm2t 5439  chdmj2t 5443  h1de2ctlem 5460  elspansnclt 5470  spansnsst 5476  osumlem1 5530  osumlem2 5531  spansncv 5542  5oalem2 5545  3oalem1 5552  pjot 5561  pjjs 5585  pjadjco 5631  pjadj2co 5656  stclt 5672  strlem3 5694  strlem4 5695  strlem5 5696  cvcon3t 5716  mdbr2 5728  dmdbr 5731  atsseq 5745  atcveq0 5746  ch1dle 5749  atom1d 5750  shatomic 5753  cvexchlem 5759  atnem0 5766  atcv0eq 5767  atcvatlem 5770  atcvat3 5774  mdsymlem2 5777  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