Theorem mpanl1 428

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 310	. 2 |- ( ps -> ( ph /\ ps ) )
3		mpanl1.2	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	2, 3	sylan 279	1 |- ( ( ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  mpanl12  430  ercnv  6380  rec11api  8374  divdiv23apzi  8386  recp1lt1  8515  divgt0i  8526  divge0i  8527  ltreci  8528  lereci  8529  lt2msqi  8530  le2msqi  8531  msq11i  8532  ltdiv23i  8542  fnn0ind  9019  elfzp1b  9718  elfzm1b  9719  sqrt11i  10744  sqrtmuli  10745  sqrtmsq2i  10747  sqrtlei  10748  sqrtlti  10749