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  6828  rec11api  9085  divdiv23apzi  9097  recp1lt1  9231  divgt0i  9242  divge0i  9243  ltreci  9244  lereci  9245  lt2msqi  9246  le2msqi  9247  msq11i  9248  ltdiv23i  9258  fnn0ind  9766  elfzp1b  10514  elfzm1b  10515  sqrt11i  11913  sqrtmuli  11914  sqrtmsq2i  11916  sqrtlei  11917  sqrtlti  11918