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  7604  m1p1sr  7958  m1m1sr  7959  0lt1sr  7963  axi2m1  8073  mul4i  8305  add4i  8322  addsub4i  8453  muladdi  8566  lt2addi  8668  le2addi  8669  mulap0i  8814  divap0i  8918  divmuldivapi  8930  divmul13api  8931  divadddivapi  8932  divdivdivapi  8933  subrecapi  8998  8th4div3  9341  iap0  9345  fldiv4p1lem1div2  10537  sqrt2gt1lt2  11575  abs3lemi  11683  3dvds2dec  12392  flodddiv4  12462  nprmi  12661  modxai  12954  sinhalfpilem  15480  cos0pilt1  15541  lgsdir2lem1  15722  lgsdir2lem5  15726  m1lgs  15779  2lgslem4  15797