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  7473  m1p1sr  7827  m1m1sr  7828  0lt1sr  7832  axi2m1  7942  mul4i  8174  add4i  8191  addsub4i  8322  muladdi  8435  lt2addi  8537  le2addi  8538  mulap0i  8683  divap0i  8787  divmuldivapi  8799  divmul13api  8800  divadddivapi  8801  divdivdivapi  8802  subrecapi  8867  8th4div3  9210  iap0  9214  fldiv4p1lem1div2  10395  sqrt2gt1lt2  11214  abs3lemi  11322  3dvds2dec  12031  flodddiv4  12101  nprmi  12292  modxai  12585  sinhalfpilem  15027  cos0pilt1  15088  lgsdir2lem1  15269  lgsdir2lem5  15273  m1lgs  15326  2lgslem4  15344