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

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  7763  m1p1sr  8117  m1m1sr  8118  0lt1sr  8122  axi2m1  8232  mul4i  8464  add4i  8481  addsub4i  8612  muladdi  8726  lt2addi  8828  le2addi  8829  mulap0i  8974  divap0i  9080  divmuldivapi  9092  divmul13api  9093  divadddivapi  9094  divdivdivapi  9095  subrecapi  9160  8th4div3  9503  iap0  9507  fldiv4p1lem1div2  10718  sqrt2gt1lt2  11793  abs3lemi  11901  3dvds2dec  12611  flodddiv4  12681  nprmi  12880  modxai  13173  sinhalfpilem  15815  cos0pilt1  15876  lgsdir2lem1  16061  lgsdir2lem5  16065  m1lgs  16118  2lgslem4  16136