Theorem syl3an3 1132

Description: A syllogism inference.

Hypotheses

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

Assertion

Ref	Expression
syl3an3	|- ((ph /\ ps /\ ta) -> th)

Proof of Theorem syl3an3

Step	Hyp	Ref	Expression
1		syl3an.1	. . . 4 |- ((ph /\ ps /\ ch) -> th)
2	1	3exp 1066	. . 3 |- (ph -> (ps -> (ch -> th)))
3		syl3an3.2	. . 3 |- (ta -> ch)
4	2, 3	syl7 26	. 2 |- (ph -> (ps -> (ta -> th)))
5	4	3imp 1061	1 |- ((ph /\ ps /\ ta) -> th)

Syntax hints:   -> wi 3   /\ w3a 858

This theorem is referenced by:  syl3an3b 1135  syl3an3br 1138  syl3anl3 1147  oprabval4g 4960  oprabval4gALT 4961  unxpdomlem 5995  addsubass 6541  subcan2 6562  subcan 6572  subsub4 6629  pnncan 6647  lesub1 6849  ltsub1 6851  divass 6924  ltmul2 7009  ltmul2OLD 7010  ltdiv2 7070  uzwo3lem1 7429  modcyc2 7517  faclbnd5 8205  serzmulc1 8317  climge0 8372  iserzmulc1 8396  climcmplem 8397  climsqueeze 8400  climsqueeze2 8401  caucvglem4 8420  caucvglem5 8421  isummulc1iALT 8474  neips 9003  opnneip 9009  lmss 9231  bcthlem1 9277  gxpval 9382  gxnn0neg 9386  gxnn0suc 9387  gxcl 9388  gxneg 9389  gxcom 9392  gxinv 9393  gxsuc 9395  gxnn0add 9397  gxadd 9398  gxsub 9399  gxnn0mul 9400  gxmul 9401  gacan 9460  minveclem26 9915  minveclem27 9916  dif1card 10177  elfilmap3 10314  hvaddsub12 10539  hvaddsubass 10542  hvsubdistr1 10548  hvsubcan 10574  hhssnv 10767  homco1 11364  homulass 11365  hoadddir 11367  hosubdi 11371  hoaddsubass 11378  hosubsub4 11381  homco2 11538  lnopmi 11562  adjlnop 11656  mdsymlem5 11979  bnj544 13270  bnj561 13283  bnj562 13284  bnj594 13300  suprzcl 13658  ndvdsp1 13712  wfrlem14 13970  sndw2 14429  gaplc 14731  hmphsyma 14882  tartarmap 15265  clsint2 15414  connsub 15443  geomcau 15849  isdivrng2 16111  lubel 16898  hlrelat5 17050  cvr1 17054  cvrp 17056

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

This theorem depends on definitions:  df-bi 164  df-an 242  df-3an 860

Copyright terms: Public domain