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  7593  m1p1sr  7947  m1m1sr  7948  0lt1sr  7952  axi2m1  8062  mul4i  8294  add4i  8311  addsub4i  8442  muladdi  8555  lt2addi  8657  le2addi  8658  mulap0i  8803  divap0i  8907  divmuldivapi  8919  divmul13api  8920  divadddivapi  8921  divdivdivapi  8922  subrecapi  8987  8th4div3  9330  iap0  9334  fldiv4p1lem1div2  10525  sqrt2gt1lt2  11560  abs3lemi  11668  3dvds2dec  12377  flodddiv4  12447  nprmi  12646  modxai  12939  sinhalfpilem  15465  cos0pilt1  15526  lgsdir2lem1  15707  lgsdir2lem5  15711  m1lgs  15764  2lgslem4  15782