Theorem mp3anl3 909

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

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

This theorem is referenced by:  mp3anr3 912  divne0bt 5691  conjmult 5753  gtndivt 6140  ioossre 6328  sq01t 6582  efaddlem10 7289  tgioolem 7853  nvcnpi4 8355  blocnilem 8395  minveclem16 8491  minveclem38 8513  nmopcoadj 9948  atcvat3 10231

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 775

Copyright terms: Public domain