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  7347  m1p1sr  7701  m1m1sr  7702  0lt1sr  7706  axi2m1  7816  mul4i  8046  add4i  8063  addsub4i  8194  muladdi  8307  lt2addi  8408  le2addi  8409  mulap0i  8553  divap0i  8656  divmuldivapi  8668  divmul13api  8669  divadddivapi  8670  divdivdivapi  8671  subrecapi  8736  8th4div3  9076  iap0  9080  fldiv4p1lem1div2  10240  sqrt2gt1lt2  10991  abs3lemi  11099  3dvds2dec  11803  flodddiv4  11871  nprmi  12056  sinhalfpilem  13352  cos0pilt1  13413  lgsdir2lem1  13569  lgsdir2lem5  13573