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  7368  m1p1sr  7722  m1m1sr  7723  0lt1sr  7727  axi2m1  7837  mul4i  8067  add4i  8084  addsub4i  8215  muladdi  8328  lt2addi  8429  le2addi  8430  mulap0i  8574  divap0i  8677  divmuldivapi  8689  divmul13api  8690  divadddivapi  8691  divdivdivapi  8692  subrecapi  8757  8th4div3  9097  iap0  9101  fldiv4p1lem1div2  10261  sqrt2gt1lt2  11013  abs3lemi  11121  3dvds2dec  11825  flodddiv4  11893  nprmi  12078  sinhalfpilem  13506  cos0pilt1  13567  lgsdir2lem1  13723  lgsdir2lem5  13727