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  7737  m1p1sr  8091  m1m1sr  8092  0lt1sr  8096  axi2m1  8206  mul4i  8437  add4i  8454  addsub4i  8585  muladdi  8699  lt2addi  8801  le2addi  8802  mulap0i  8947  divap0i  9051  divmuldivapi  9063  divmul13api  9064  divadddivapi  9065  divdivdivapi  9066  subrecapi  9131  8th4div3  9474  iap0  9478  fldiv4p1lem1div2  10689  sqrt2gt1lt2  11759  abs3lemi  11867  3dvds2dec  12577  flodddiv4  12647  nprmi  12846  modxai  13139  sinhalfpilem  15782  cos0pilt1  15843  lgsdir2lem1  16027  lgsdir2lem5  16031  m1lgs  16084  2lgslem4  16102