Theorem mpanl2 705

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 694	. 2 |- (ph -> (ch -> th))
5	4	imp 350	1 |- ((ph /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  mp3an2 901  reuss 2266  limom 3136  tfrlem11 3906  tfr3 3911  oe0 4145  infensuc 4610  noinfep 4612  indpi 5006  prlem934b 5110  axcnre 5258  muleqaddt 5669  ledivp1 5854  ltdivp1 5855  supxrpnf 6035  supxrunb1 6036  supxrunb2 6037  eigpos 9679  nmopco 9942  nmopcoadj 9948  hstrb 10103  mapudiscn 10399

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