Theorem mpanr2 714

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 371	. . 3 |- (ph -> ((ps /\ ch) -> th))
4	1, 3	mpan2i 703	. 2 |- (ph -> (ps -> th))
5	4	imp 348	1 |- ((ph /\ ps) -> th)

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  pm54.43 4715  aceq6b 4888  prlem934b 5292  muleqadd 5852  divdiv1 5934  rimul 6945  isumcmpii 7419  opnneissb 7938  blssopn 8077  blnei 8089  va1cnlem 8599  blocnilem 8719  sineq0OLD 8984  lnopmul 10170  subsubtop 11479  fneref 11554  fiinbas 11905  iimulcl 11938  hmeocld 11961

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 145  df-an 223

Copyright terms: Public domain