Theorem mpanl1 434

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  436  ercnv  6790  rec11api  9029  divdiv23apzi  9041  recp1lt1  9175  divgt0i  9186  divge0i  9187  ltreci  9188  lereci  9189  lt2msqi  9190  le2msqi  9191  msq11i  9192  ltdiv23i  9202  fnn0ind  9697  elfzp1b  10435  elfzm1b  10436  sqrt11i  11821  sqrtmuli  11822  sqrtmsq2i  11824  sqrtlei  11825  sqrtlti  11826