Theorem mp4an 427

Description: An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2011.)

Hypotheses

Ref	Expression
mp4an.1	⊢ 𝜑
mp4an.2	⊢ 𝜓
mp4an.3	⊢ 𝜒
mp4an.4	⊢ 𝜃
mp4an.5	⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)

Assertion

Ref	Expression
mp4an	⊢ 𝜏

Proof of Theorem mp4an

Step	Hyp	Ref	Expression
1		mp4an.1	. . 3 ⊢ 𝜑
2		mp4an.2	. . 3 ⊢ 𝜓
3	1, 2	pm3.2i 272	. 2 ⊢ (𝜑 ∧ 𝜓)
4		mp4an.3	. . 3 ⊢ 𝜒
5		mp4an.4	. . 3 ⊢ 𝜃
6	4, 5	pm3.2i 272	. 2 ⊢ (𝜒 ∧ 𝜃)
7		mp4an.5	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
8	3, 6, 7	mp2an 426	1 ⊢ 𝜏

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  7616  m1p1sr  7970  m1m1sr  7971  0lt1sr  7975  axi2m1  8085  mul4i  8317  add4i  8334  addsub4i  8465  muladdi  8578  lt2addi  8680  le2addi  8681  mulap0i  8826  divap0i  8930  divmuldivapi  8942  divmul13api  8943  divadddivapi  8944  divdivdivapi  8945  subrecapi  9010  8th4div3  9353  iap0  9357  fldiv4p1lem1div2  10555  sqrt2gt1lt2  11600  abs3lemi  11708  3dvds2dec  12417  flodddiv4  12487  nprmi  12686  modxai  12979  sinhalfpilem  15505  cos0pilt1  15566  lgsdir2lem1  15747  lgsdir2lem5  15751  m1lgs  15804  2lgslem4  15822