Theorem mpanl2 771

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

Hypotheses

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

Assertion

Ref	Expression
mpanl2	|- ((ph /\ ch) -> th)

Proof of Theorem mpanl2

Step	Hyp	Ref	Expression
1		mpanl2.1	. 2 |- ps
2		mpanl2.2	. . 3 |- (((ph /\ ps) /\ ch) -> th)
3	2	an1rs 547	. 2 |- (((ph /\ ch) /\ ps) -> th)
4	1, 3	mpan2 760	1 |- ((ph /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  mpanr1 774  mp3an2 1179  reuss 2871  limom 3967  tfrlem11 5129  tfr3 5134  oe0 5206  infensuc 5745  noinfep 5747  indpi 6186  prlem934b 6290  axcnre 6439  muleqadd 6889  divdiv2 6973  ledivp1i 7089  addltmul 7229  supxrpnf 7297  supxrunb1 7298  supxrunb2 7299  spwpr4 10006  spwpr4OLD 10007  spwpr4aOLD 10008  sineq0OLD 10066  dif1en 10172  eigposi 11399  nmopcoi 11665  nmopcoadji 11671  opsqrlem6 11716  hstrbi 11838  mapudiscn 14872  iimulcl 15874  pcohtpy 16083  pi1gp 16095

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