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  7466  m1p1sr  7820  m1m1sr  7821  0lt1sr  7825  axi2m1  7935  mul4i  8167  add4i  8184  addsub4i  8315  muladdi  8428  lt2addi  8529  le2addi  8530  mulap0i  8675  divap0i  8779  divmuldivapi  8791  divmul13api  8792  divadddivapi  8793  divdivdivapi  8794  subrecapi  8859  8th4div3  9201  iap0  9205  fldiv4p1lem1div2  10374  sqrt2gt1lt2  11193  abs3lemi  11301  3dvds2dec  12007  flodddiv4  12075  nprmi  12262  sinhalfpilem  14926  cos0pilt1  14987  lgsdir2lem1  15144  lgsdir2lem5  15148  m1lgs  15192