Theorem mp4an 417

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 266	. 2 |- ( ph /\ ps )
4		mp4an.3	. . 3 |- ch
5		mp4an.4	. . 3 |- th
6	4, 5	pm3.2i 266	. 2 |- ( ch /\ th )
7		mp4an.5	. 2 |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )
8	3, 6, 7	mp2an 416	1 |- ta

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  1lt2nq  6596  m1p1sr  6937  m1m1sr  6938  0lt1sr  6942  axi2m1  7041  mul4i  7256  add4i  7273  addsub4i  7404  muladdi  7513  lt2addi  7611  le2addi  7612  mulap0i  7746  divap0i  7848  divmuldivapi  7860  divmul13api  7861  divadddivapi  7862  divdivdivapi  7863  8th4div3  8250  iap0  8254  fldiv4p1lem1div2  9307  sqrt2gt1lt2  9935  abs3lemi  10043  3dvds2dec  10265  flodddiv4  10334  nprmi  10506