Theorem mp3anl3 912

Description: An inference based on modus ponens.

Hypotheses

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

Assertion

Ref	Expression
mp3anl3	|- (((ph /\ ps) /\ th) -> ta)

Proof of Theorem mp3anl3

Step	Hyp	Ref	Expression
1		mp3anl3.1	. . 3 |- ch
2		mp3anl3.2	. . . 4 |- (((ph /\ ps /\ ch) /\ th) -> ta)
3	2	ex 373	. . 3 |- ((ph /\ ps /\ ch) -> (th -> ta))
4	1, 3	mp3an3 905	. 2 |- ((ph /\ ps) -> (th -> ta))
5	4	imp 350	1 |- (((ph /\ ps) /\ th) -> ta)

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 775

This theorem is referenced by:  mp3anr3 915  divne0bt 5728  conjmult 5797  gtndivt 6193  sq01t 6651  efaddlem10 7347  tgioolem 7914  nvcnpi3 8422  nvcnpi4 8423  blocnilem 8464  minveclem16 8560  minveclem38 8582  nmopcoadj 10034  atcvat3 10323

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  df-3an 777

Copyright terms: Public domain