Theorem mpanr2 710

Description: An inference based on modus ponens.

Hypotheses

Ref	Expression
mpanr2.1	|- ch
mpanr2.2	|- ((ph /\ (ps /\ ch)) -> th)

Assertion

Ref	Expression
mpanr2	|- ((ph /\ ps) -> th)

Proof of Theorem mpanr2

Step	Hyp	Ref	Expression
1		mpanr2.1	. . 3 |- ch
2		mpanr2.2	. . . 4 |- ((ph /\ (ps /\ ch)) -> th)
3	2	ex 373	. . 3 |- (ph -> ((ps /\ ch) -> th))
4	1, 3	mpan2i 699	. 2 |- (ph -> (ps -> th))
5	4	imp 350	1 |- ((ph /\ ps) -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  pm54.43 4572  aceq6b 4742  prlem934b 5138  muleqaddt 5700  rimul 6744  isumcmpi 7215  opnneissb 7728  blssopn 7867  blnei 7879  va1cnlem 8345  blocnilem 8464  sineq0 8713  lnopmult 9891

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain