Theorem sylanc 361

Description: A syllogism inference combined with contraction.

Hypotheses

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

Assertion

Ref	Expression
sylanc	|- (th -> ch)

Proof of Theorem sylanc

Step	Hyp	Ref	Expression
1		sylanc.1	. . 3 |- ((ph /\ ps) -> ch)
2	1	exp 291	. 2 |- (ph -> (ps -> ch))
3		sylanc.2	. 2 |- (th -> ph)
4		sylanc.3	. 2 |- (th -> ps)
5	2, 3, 4	sylc 62	1 |- (th -> ch)

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  anim12d 431  orim12d 436  pm5.21ni 503  eueq2 1429  eueq3 1430  sbc2or 1454  sstrd 1513  ralidm 1774  raaan 1775  exss 1881  supub 2160  suplub 2161  ordelord 2221  onfr 2237  onnmin 2270  onminex 2275  onmindif2 2313  limsssuc 2362  peano5 2394  funfni 2724  fnresdm 2731  f1ores 2813  tfrlem12 2960  tz7.48-2 2995  2dom 3332  undom 3342  xpassen 3344  sbthlem8 3356  mapunen 3397  limenpsi 3400  limensuci 3401  php3 3411  onomeneq 3414  unblem4 3434  unbnn 3435  r1ord 3499  rankr1 3518  fodom 3613  unxpdomlem 3649  unxpdom2 3651  cardalephex 3691  cfsuc 3709  cdafi 3730  axrepnd 3740  indpi 3828  addpipq 3848  halfpq 3876  ltaddpr 3934  ltexprlem2 3937  mulsrpr 3979  negexsr 4005  mulgt0sr 4008  mulcnsr 4048  mulresr 4051  axmulcl 4068  ax1id 4077  axnegex 4078  axrecex 4079  axcnre 4087  addsubasst 4150  divmuldivt 4263  divdivdivt 4265  divdiv23t 4271  lt2sq 4414  nnge1t 4439  nnleltp1t 4448  suprub 4513  nnreclt 4522  nn0ltp1let 4556  zltp1let 4597  uzind 4603  flidt 4627  qaddclt 4642  qmulclt 4644  seqlem1 4662  seqlem2 4663  seqrval 4664  seqsuclem 4669  expaddt 4698  cjclt 4800  ruclem13 4897  xpnnen 4927  znnenlem 4929  infxpidmlem1 4933  infxpidmlem11 4943  infxpidmlem12 4944  infunabs 4946  infcdaabs 4947  infdif 4948  alephexp1 4954  alephsuc3 4955  hvsubcan1t 5016  his2subt 5052  hi2eqt 5059  normclt 5076  normge0t 5077  normgt0t 5078  chocuni 5179  projlem2 5194  projlem25 5217  projlem26 5218  projlem28 5220  projlem30 5222  pjthlem7 5231  pjpjtht 5262  pjpot 5265  pjoml 5271  shscl 5282  hsupval2t 5301  spanssoc 5320  shunss 5338  chabs1t 5432  spanunsn 5482  h1datom 5483  osumlem6 5535  osumlem7 5536  spansncv 5542  5oalem1 5544  5oalem2 5545  3oalem2 5553  pjrn 5587  hosf 5602  hodf 5603  hoscom 5605  pjsdi 5625  pjddi 5626  pjss2co 5634  pjclem4 5653  pj3s 5659  pj3cor1 5661  pjelt 5668  sto2 5678  stadd 5687  stadd3 5689  strlem1 5691  str 5698  golem1 5704  stcltrlem1 5709  spansncv2t 5725  atom1d 5750  chcv1t 5751  shatomic 5753  cvp 5764  atcv0eq 5767  atexch 5769  atcvat4 5775  mdsymlem2 5777  mdsymlem6 5781

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