Theorem mp4an 427

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  1lt2nq  7490  m1p1sr  7844  m1m1sr  7845  0lt1sr  7849  axi2m1  7959  mul4i  8191  add4i  8208  addsub4i  8339  muladdi  8452  lt2addi  8554  le2addi  8555  mulap0i  8700  divap0i  8804  divmuldivapi  8816  divmul13api  8817  divadddivapi  8818  divdivdivapi  8819  subrecapi  8884  8th4div3  9227  iap0  9231  fldiv4p1lem1div2  10412  sqrt2gt1lt2  11231  abs3lemi  11339  3dvds2dec  12048  flodddiv4  12118  nprmi  12317  modxai  12610  sinhalfpilem  15111  cos0pilt1  15172  lgsdir2lem1  15353  lgsdir2lem5  15357  m1lgs  15410  2lgslem4  15428