Theorem mp3anl1 909

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

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

This theorem is referenced by:  mp3anr1 912  rec11rt 5745  ltmulgt11t 5812  gt0divt 5817  ge0divt 5818  ledivp1 5864  ltdivp1 5865  qbtwnre 6228  ioossre 6341  facwordit 6896  facavgt 6907  efaddlem5 7301  methausi 7843  tgioolem 7876  xplmi 7935  xplm 7937  xpcn 7938  bcthlem13 7973  bcthlem14 7974  bcthlem19 7979  bcthlem26 7986  nmobndi 8398  blometi 8422  blocnilem 8423  ubthlem3 8490  ubthlem9 8496  ubthlem10 8497  ubthlem11 8498  mdslmd3 10215  atcvat2 10270  irredlem3 10275  mdsymlem1 10286  cdj1 10316

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 776

Copyright terms: Public domain