Theorem mp4an 418

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 266	. 2 |- ( ph /\ ps )
4		mp4an.3	. . 3 |- ch
5		mp4an.4	. . 3 |- th
6	4, 5	pm3.2i 266	. 2 |- ( ch /\ th )
7		mp4an.5	. 2 |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )
8	3, 6, 7	mp2an 417	1 |- ta

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106

This theorem is referenced by:  1lt2nq  6963  m1p1sr  7304  m1m1sr  7305  0lt1sr  7309  axi2m1  7408  mul4i  7628  add4i  7645  addsub4i  7776  muladdi  7885  lt2addi  7986  le2addi  7987  mulap0i  8123  divap0i  8225  divmuldivapi  8237  divmul13api  8238  divadddivapi  8239  divdivdivapi  8240  8th4div3  8633  iap0  8637  fldiv4p1lem1div2  9708  sqrt2gt1lt2  10478  abs3lemi  10586  3dvds2dec  11140  flodddiv4  11208  nprmi  11380