Theorem mp3anr1 910

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 436	. . 3 |- (((ps /\ ch /\ th) /\ ph) -> ta)
4	1, 3	mp3anl1 907	. 2 |- (((ch /\ th) /\ ph) -> ta)
5	4	ancoms 436	1 |- ((ph /\ (ch /\ th)) -> ta)

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

This theorem is referenced by:  recdivt 5746  vc2 8111  vcsubdir 8112  vc0 8125  vcm 8127  vcnegneg 8130  vcnegsubdi2 8131  vcsub4 8132  nvaddsub4 8221  nvnncan 8223  nvpi 8233  nvge0 8241  ipval3 8293  ipid 8297  ipsubdir 8439

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