Theorem mp3anl1 907

Description: An inference based on modus ponens.

Hypotheses

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

Assertion

Ref	Expression
mp3anl1	|- (((ps /\ ch) /\ th) -> ta)

Proof of Theorem mp3anl1

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

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

This theorem is referenced by:  mp3anr1 910  rec11rt 5735  ltmulgt11t 5802  gt0divt 5807  ge0divt 5808  ledivp1 5854  ltdivp1 5855  qbtwnre 6216  ioossre 6328  facwordit 6881  facavgt 6892  efaddlem5 7284  methausi 7820  tgioolem 7853  xplmi 7907  xplm 7909  xpcn 7910  bcthlem13 7945  bcthlem14 7946  bcthlem19 7951  bcthlem26 7958  nmobndi 8370  blometi 8394  blocnilem 8395  ubthlem3 8462  ubthlem9 8468  ubthlem10 8469  ubthlem11 8470  mdslmd3 10167  atcvat2 10222  irredlem3 10227  mdsymlem1 10238  cdj1 10265

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