Theorem mp4an 425

Description: An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2011.)

Hypotheses

Ref	Expression
mp4an.1	|- ph
mp4an.2	|- ps
mp4an.3	|- ch
mp4an.4	|- th
mp4an.5	|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )

Assertion

Ref	Expression
mp4an	|- ta

Proof of Theorem mp4an

Step	Hyp	Ref	Expression
1		mp4an.1	. . 3 |- ph
2		mp4an.2	. . 3 |- ps
3	1, 2	pm3.2i 270	. 2 |- ( ph /\ ps )
4		mp4an.3	. . 3 |- ch
5		mp4an.4	. . 3 |- th
6	4, 5	pm3.2i 270	. 2 |- ( ch /\ th )
7		mp4an.5	. 2 |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )
8	3, 6, 7	mp2an 424	1 |- ta

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  1lt2nq  7355  m1p1sr  7709  m1m1sr  7710  0lt1sr  7714  axi2m1  7824  mul4i  8054  add4i  8071  addsub4i  8202  muladdi  8315  lt2addi  8416  le2addi  8417  mulap0i  8561  divap0i  8664  divmuldivapi  8676  divmul13api  8677  divadddivapi  8678  divdivdivapi  8679  subrecapi  8744  8th4div3  9084  iap0  9088  fldiv4p1lem1div2  10248  sqrt2gt1lt2  11000  abs3lemi  11108  3dvds2dec  11812  flodddiv4  11880  nprmi  12065  sinhalfpilem  13465  cos0pilt1  13526  lgsdir2lem1  13682  lgsdir2lem5  13686