Theorem mp3an2 640

Description: An inference based on modus ponens.

Hypotheses

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

Assertion

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

Proof of Theorem mp3an2

Step	Hyp	Ref	Expression
1		mp3an2.1	. 2 |- ps
2		mp3an2.2	. . 3 |- ((ph /\ ps /\ ch) -> th)
3	2	3expa 612	. 2 |- (((ph /\ ps) /\ ch) -> th)
4	1, 3	mpan12 530	1 |- ((ph /\ ch) -> th)

Syntax hints:   -> wi 2   /\ wa 196   /\ w3a 581

This theorem is referenced by:  ordin 2228  1qec 3862  nnsub 4450  nnaddm1clt 4452  nnunb 4520  lt0nnn0 4549  zltp1let 4597  zbtwnre 4619  rebtwnz 4620  nn0ennn 4925  znnenlem 4929  hvmul0t 5004  occllem6 5185  projlem26 5218  pjthlem6 5230  h1de2b 5459  mdsymlem5 5780

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  df-3an 583

metamath.org