Theorem mp4an 424

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 270	. 2 ⊢ (𝜑 ∧ 𝜓)
4		mp4an.3	. . 3 ⊢ 𝜒
5		mp4an.4	. . 3 ⊢ 𝜃
6	4, 5	pm3.2i 270	. 2 ⊢ (𝜒 ∧ 𝜃)
7		mp4an.5	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
8	3, 6, 7	mp2an 423	1 ⊢ 𝜏

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  1lt2nq  7338  m1p1sr  7692  m1m1sr  7693  0lt1sr  7697  axi2m1  7807  mul4i  8037  add4i  8054  addsub4i  8185  muladdi  8298  lt2addi  8399  le2addi  8400  mulap0i  8544  divap0i  8647  divmuldivapi  8659  divmul13api  8660  divadddivapi  8661  divdivdivapi  8662  subrecapi  8727  8th4div3  9067  iap0  9071  fldiv4p1lem1div2  10230  sqrt2gt1lt2  10977  abs3lemi  11085  3dvds2dec  11788  flodddiv4  11856  nprmi  12035  sinhalfpilem  13253  cos0pilt1  13314