Theorem mp4an 431

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 430	1 |- ta

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  1lt2nq  7773  m1p1sr  8127  m1m1sr  8128  0lt1sr  8132  axi2m1  8242  mul4i  8475  add4i  8492  addsub4i  8623  muladdi  8737  lt2addi  8839  le2addi  8840  mulap0i  8986  divap0i  9092  divmuldivapi  9104  divmul13api  9105  divadddivapi  9106  divdivdivapi  9107  subrecapi  9172  8th4div3  9528  iap0  9532  fldiv4p1lem1div2  10753  sqrt2gt1lt2  11829  abs3lemi  11938  3dvds2dec  12649  flodddiv4  12719  nprmi  12918  modxai  13215  mod2xnegi  13218  sinhalfpilem  15942  cos0pilt1  16003  log2tlbndlog2  16139  log2ublog2  16143  ppiqub  16194  lgsdir2lem1  16245  lgsdir2lem5  16249  m1lgs  16302  2lgslem4  16320