Theorem mpanl1 438

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  440  ercnv  6818  rec11api  9073  divdiv23apzi  9085  recp1lt1  9219  divgt0i  9230  divge0i  9231  ltreci  9232  lereci  9233  lt2msqi  9234  le2msqi  9235  msq11i  9236  ltdiv23i  9246  fnn0ind  9741  elfzp1b  10482  elfzm1b  10483  sqrt11i  11876  sqrtmuli  11877  sqrtmsq2i  11879  sqrtlei  11880  sqrtlti  11881