Theorem mpanl2 706

Description: An inference based on modus ponens.

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	. . 3 |- ps
2		mpanl2.2	. . . 4 |- (((ph /\ ps) /\ ch) -> th)
3	2	ex 373	. . 3 |- ((ph /\ ps) -> (ch -> th))
4	1, 3	mpan2 695	. 2 |- (ph -> (ch -> th))
5	4	imp 350	1 |- ((ph /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  mp3an2 902  reuss 2272  limom 3141  tfrlem11 3912  tfr3 3917  oe0 4151  infensuc 4618  noinfep 4620  indpi 5014  prlem934b 5118  axcnre 5266  muleqaddt 5677  ledivp1 5862  ltdivp1 5863  supxrpnf 6043  supxrunb1 6044  supxrunb2 6045  eigpos 9702  nmopco 9966  nmopcoadj 9972  hstrb 10131  mapudiscn 10435

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