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  7721  m1p1sr  8075  m1m1sr  8076  0lt1sr  8080  axi2m1  8190  mul4i  8421  add4i  8438  addsub4i  8569  muladdi  8682  lt2addi  8784  le2addi  8785  mulap0i  8930  divap0i  9034  divmuldivapi  9046  divmul13api  9047  divadddivapi  9048  divdivdivapi  9049  subrecapi  9114  8th4div3  9457  iap0  9461  fldiv4p1lem1div2  10665  sqrt2gt1lt2  11734  abs3lemi  11842  3dvds2dec  12552  flodddiv4  12622  nprmi  12821  modxai  13114  sinhalfpilem  15656  cos0pilt1  15717  lgsdir2lem1  15901  lgsdir2lem5  15905  m1lgs  15958  2lgslem4  15976