Theorem mpanr2 776

Description: An inference based on modus ponens. (The proof was shortened by Andrew Salmon, 7-May-2011.)

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	. 2 |- ch
2		mpanr2.2	. . 3 |- ((ph /\ (ps /\ ch)) -> th)
3	2	anassrs 489	. 2 |- (((ph /\ ps) /\ ch) -> th)
4	1, 3	mpan2 760	1 |- ((ph /\ ps) -> th)

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  pm54.43 5662  aceq6b 5904  prlem934b 6290  muleqadd 6889  divdiv1 6972  addltmul 7229  rimul 7994  isumcmpii 8476  fiinbas 8885  opnneissb 9004  blssopn 9144  blnei 9156  va1cnlem 9684  blocnilem 9804  sineq0OLD 10066  lnopmul 11528  opsqrlem6 11716  elfzp1b 13605  elfzm1b 13606  subsubtop 15423  fneref 15493  fdc 15812  iimulcl 15874  hmeocld 15900  elpi1i 16090  linepmap 17249

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 164  df-an 242

Copyright terms: Public domain