Theorem mp4an 423

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 422	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  7214  m1p1sr  7568  m1m1sr  7569  0lt1sr  7573  axi2m1  7683  mul4i  7910  add4i  7927  addsub4i  8058  muladdi  8171  lt2addi  8272  le2addi  8273  mulap0i  8417  divap0i  8520  divmuldivapi  8532  divmul13api  8533  divadddivapi  8534  divdivdivapi  8535  subrecapi  8599  8th4div3  8939  iap0  8943  fldiv4p1lem1div2  10078  sqrt2gt1lt2  10821  abs3lemi  10929  3dvds2dec  11563  flodddiv4  11631  nprmi  11805  sinhalfpilem  12872