Theorem mp3anl3 914

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

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

This theorem is referenced by:  mp3anr3 917  divne0bt 5735  conjmult 5799  gtndivt 6195  sq01t 6652  efaddlem10 7347  tgioolem 7911  nvcnpi3 8418  nvcnpi4 8419  blocnilem 8460  minveclem16 8556  minveclem38 8578  nmopcoadj 10029  atcvat3 10318

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 779

Copyright terms: Public domain