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  10760  sqrt2gt1lt2  11836  abs3lemi  11945  3dvds2dec  12657  flodddiv4  12727  nprmi  12926  modxai  13223  mod2xnegi  13226  sinhalfpilem  16035  cos0pilt1  16097  log2tlbndlog2  16237  log2ublog2  16241  ppiqub  16310  bposlem8  16335  bposlem9  16336  lgsdir2lem1  16369  lgsdir2lem5  16373  m1lgs  16426  2lgslem4  16444