Theorem mpanl1 430

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  432  ercnv  6443  rec11api  8506  divdiv23apzi  8518  recp1lt1  8650  divgt0i  8661  divge0i  8662  ltreci  8663  lereci  8664  lt2msqi  8665  le2msqi  8666  msq11i  8667  ltdiv23i  8677  fnn0ind  9160  elfzp1b  9870  elfzm1b  9871  sqrt11i  10897  sqrtmuli  10898  sqrtmsq2i  10900  sqrtlei  10901  sqrtlti  10902