Theorem mpanl1 432

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  434  ercnv  6534  rec11api  8670  divdiv23apzi  8682  recp1lt1  8815  divgt0i  8826  divge0i  8827  ltreci  8828  lereci  8829  lt2msqi  8830  le2msqi  8831  msq11i  8832  ltdiv23i  8842  fnn0ind  9328  elfzp1b  10053  elfzm1b  10054  sqrt11i  11096  sqrtmuli  11097  sqrtmsq2i  11099  sqrtlei  11100  sqrtlti  11101