Theorem mpanl1 425

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  mpanl12  427  ercnv  6214  rec11api  7960  divdiv23apzi  7972  recp1lt1  8096  divgt0i  8107  divge0i  8108  ltreci  8109  lereci  8110  lt2msqi  8111  le2msqi  8112  msq11i  8113  ltdiv23i  8123  fnn0ind  8596  elfzp1b  9242  elfzm1b  9243  sqrt11i  10219  sqrtmuli  10220  sqrtmsq2i  10222  sqrtlei  10223  sqrtlti  10224