Theorem mp4an 424

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 423	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  7238  m1p1sr  7592  m1m1sr  7593  0lt1sr  7597  axi2m1  7707  mul4i  7934  add4i  7951  addsub4i  8082  muladdi  8195  lt2addi  8296  le2addi  8297  mulap0i  8441  divap0i  8544  divmuldivapi  8556  divmul13api  8557  divadddivapi  8558  divdivdivapi  8559  subrecapi  8623  8th4div3  8963  iap0  8967  fldiv4p1lem1div2  10109  sqrt2gt1lt2  10853  abs3lemi  10961  3dvds2dec  11599  flodddiv4  11667  nprmi  11841  sinhalfpilem  12920  cos0pilt1  12981