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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  mpanl12  440  ercnv  6832  rec11api  9091  divdiv23apzi  9103  recp1lt1  9237  divgt0i  9248  divge0i  9249  ltreci  9250  lereci  9251  lt2msqi  9252  le2msqi  9253  msq11i  9254  ltdiv23i  9264  fnn0ind  9773  elfzp1b  10521  elfzm1b  10522  sqrt11i  11921  sqrtmuli  11922  sqrtmsq2i  11924  sqrtlei  11925  sqrtlti  11926