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  8474  add4i  8491  addsub4i  8622  muladdi  8736  lt2addi  8838  le2addi  8839  mulap0i  8984  divap0i  9090  divmuldivapi  9102  divmul13api  9103  divadddivapi  9104  divdivdivapi  9105  subrecapi  9170  8th4div3  9524  iap0  9528  fldiv4p1lem1div2  10740  sqrt2gt1lt2  11815  abs3lemi  11923  3dvds2dec  12633  flodddiv4  12703  nprmi  12902  modxai  13195  sinhalfpilem  15892  cos0pilt1  15953  log2tlbndlog2  16082  log2ublog2  16086  lgsdir2lem1  16147  lgsdir2lem5  16151  m1lgs  16204  2lgslem4  16222