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  7435  m1p1sr  7789  m1m1sr  7790  0lt1sr  7794  axi2m1  7904  mul4i  8135  add4i  8152  addsub4i  8283  muladdi  8396  lt2addi  8497  le2addi  8498  mulap0i  8643  divap0i  8747  divmuldivapi  8759  divmul13api  8760  divadddivapi  8761  divdivdivapi  8762  subrecapi  8827  8th4div3  9168  iap0  9172  fldiv4p1lem1div2  10336  sqrt2gt1lt2  11090  abs3lemi  11198  3dvds2dec  11903  flodddiv4  11971  nprmi  12156  sinhalfpilem  14669  cos0pilt1  14730  lgsdir2lem1  14887  lgsdir2lem5  14891  m1lgs  14910