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  7779  m1p1sr  8133  m1m1sr  8134  0lt1sr  8138  axi2m1  8248  mul4i  8481  add4i  8498  addsub4i  8629  muladdi  8743  lt2addi  8845  le2addi  8846  mulap0i  8992  divap0i  9098  divmuldivapi  9110  divmul13api  9111  divadddivapi  9112  divdivdivapi  9113  subrecapi  9178  8th4div3  9535  iap0  9539  fldiv4p1lem1div2  10761  sqrt2gt1lt2  11837  abs3lemi  11946  3dvds2dec  12658  flodddiv4  12728  nprmi  12927  modxai  13224  mod2xnegi  13227  sinhalfpilem  16018  cos0pilt1  16080  log2tlbndlog2  16220  log2ublog2  16224  ppiqub  16293  bposlem8  16318  bposlem9  16319  lgsdir2lem1  16352  lgsdir2lem5  16356  m1lgs  16409  2lgslem4  16427