Theorem mpanl1 431

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  mpanl12  433  ercnv  6522  rec11api  8649  divdiv23apzi  8661  recp1lt1  8794  divgt0i  8805  divge0i  8806  ltreci  8807  lereci  8808  lt2msqi  8809  le2msqi  8810  msq11i  8811  ltdiv23i  8821  fnn0ind  9307  elfzp1b  10032  elfzm1b  10033  sqrt11i  11074  sqrtmuli  11075  sqrtmsq2i  11077  sqrtlei  11078  sqrtlti  11079