Theorem mp3anr1 915

Description: An inference based on modus ponens.

Hypotheses

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

Assertion

Ref	Expression
mp3anr1	|- ((ph /\ (ch /\ th)) -> ta)

Proof of Theorem mp3anr1

Step	Hyp	Ref	Expression
1		mp3anr1.1	. . 3 |- ps
2		mp3anr1.2	. . . 4 |- ((ph /\ (ps /\ ch /\ th)) -> ta)
3	2	ancoms 438	. . 3 |- (((ps /\ ch /\ th) /\ ph) -> ta)
4	1, 3	mp3anl1 912	. 2 |- (((ch /\ th) /\ ph) -> ta)
5	4	ancoms 438	1 |- ((ph /\ (ch /\ th)) -> ta)

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

This theorem is referenced by:  recdivt 5792  vc2 8170  vcsubdir 8171  vc0 8184  vcm 8186  vcnegneg 8189  vcnegsubdi2 8190  vcsub4 8191  nvaddsub4 8277  nvnncan 8279  nvpi 8290  nvge0 8298  ipval3 8355  ipid 8359  ipsubdir 8504

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