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  7519  m1p1sr  7873  m1m1sr  7874  0lt1sr  7878  axi2m1  7988  mul4i  8220  add4i  8237  addsub4i  8368  muladdi  8481  lt2addi  8583  le2addi  8584  mulap0i  8729  divap0i  8833  divmuldivapi  8845  divmul13api  8846  divadddivapi  8847  divdivdivapi  8848  subrecapi  8913  8th4div3  9256  iap0  9260  fldiv4p1lem1div2  10448  sqrt2gt1lt2  11360  abs3lemi  11468  3dvds2dec  12177  flodddiv4  12247  nprmi  12446  modxai  12739  sinhalfpilem  15263  cos0pilt1  15324  lgsdir2lem1  15505  lgsdir2lem5  15509  m1lgs  15562  2lgslem4  15580