Theorem mp4an 421

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  1lt2nq  7115  m1p1sr  7456  m1m1sr  7457  0lt1sr  7461  axi2m1  7560  mul4i  7781  add4i  7798  addsub4i  7929  muladdi  8038  lt2addi  8139  le2addi  8140  mulap0i  8278  divap0i  8381  divmuldivapi  8393  divmul13api  8394  divadddivapi  8395  divdivdivapi  8396  8th4div3  8791  iap0  8795  fldiv4p1lem1div2  9919  sqrt2gt1lt2  10661  abs3lemi  10769  3dvds2dec  11358  flodddiv4  11426  nprmi  11598