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  7686  m1p1sr  8040  m1m1sr  8041  0lt1sr  8045  axi2m1  8155  mul4i  8386  add4i  8403  addsub4i  8534  muladdi  8647  lt2addi  8749  le2addi  8750  mulap0i  8895  divap0i  8999  divmuldivapi  9011  divmul13api  9012  divadddivapi  9013  divdivdivapi  9014  subrecapi  9079  8th4div3  9422  iap0  9426  fldiv4p1lem1div2  10628  sqrt2gt1lt2  11689  abs3lemi  11797  3dvds2dec  12507  flodddiv4  12577  nprmi  12776  modxai  13069  sinhalfpilem  15602  cos0pilt1  15663  lgsdir2lem1  15847  lgsdir2lem5  15851  m1lgs  15904  2lgslem4  15922