Theorem mp4an 427

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 426	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  7554  m1p1sr  7908  m1m1sr  7909  0lt1sr  7913  axi2m1  8023  mul4i  8255  add4i  8272  addsub4i  8403  muladdi  8516  lt2addi  8618  le2addi  8619  mulap0i  8764  divap0i  8868  divmuldivapi  8880  divmul13api  8881  divadddivapi  8882  divdivdivapi  8883  subrecapi  8948  8th4div3  9291  iap0  9295  fldiv4p1lem1div2  10485  sqrt2gt1lt2  11475  abs3lemi  11583  3dvds2dec  12292  flodddiv4  12362  nprmi  12561  modxai  12854  sinhalfpilem  15378  cos0pilt1  15439  lgsdir2lem1  15620  lgsdir2lem5  15624  m1lgs  15677  2lgslem4  15695