Theorem mpanl1 434

Description: An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

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

Assertion

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

Proof of Theorem mpanl1

Step	Hyp	Ref	Expression
1		mpanl1.1	. . 3 |- ph
2	1	jctl 314	. 2 |- ( ps -> ( ph /\ ps ) )
3		mpanl1.2	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	2, 3	sylan 283	1 |- ( ( ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  mpanl12  436  ercnv  6801  rec11api  9044  divdiv23apzi  9056  recp1lt1  9190  divgt0i  9201  divge0i  9202  ltreci  9203  lereci  9204  lt2msqi  9205  le2msqi  9206  msq11i  9207  ltdiv23i  9217  fnn0ind  9712  elfzp1b  10453  elfzm1b  10454  sqrt11i  11842  sqrtmuli  11843  sqrtmsq2i  11845  sqrtlei  11846  sqrtlti  11847