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  7521  m1p1sr  7875  m1m1sr  7876  0lt1sr  7880  axi2m1  7990  mul4i  8222  add4i  8239  addsub4i  8370  muladdi  8483  lt2addi  8585  le2addi  8586  mulap0i  8731  divap0i  8835  divmuldivapi  8847  divmul13api  8848  divadddivapi  8849  divdivdivapi  8850  subrecapi  8915  8th4div3  9258  iap0  9262  fldiv4p1lem1div2  10450  sqrt2gt1lt2  11393  abs3lemi  11501  3dvds2dec  12210  flodddiv4  12280  nprmi  12479  modxai  12772  sinhalfpilem  15296  cos0pilt1  15357  lgsdir2lem1  15538  lgsdir2lem5  15542  m1lgs  15595  2lgslem4  15613