Theorem mpanl1 431

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  433  ercnv  6513  rec11api  8640  divdiv23apzi  8652  recp1lt1  8785  divgt0i  8796  divge0i  8797  ltreci  8798  lereci  8799  lt2msqi  8800  le2msqi  8801  msq11i  8802  ltdiv23i  8812  fnn0ind  9298  elfzp1b  10022  elfzm1b  10023  sqrt11i  11060  sqrtmuli  11061  sqrtmsq2i  11063  sqrtlei  11064  sqrtlti  11065