Theorem mp4an 418

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  1lt2nq  6647  m1p1sr  6988  m1m1sr  6989  0lt1sr  6993  axi2m1  7092  mul4i  7312  add4i  7329  addsub4i  7460  muladdi  7569  lt2addi  7667  le2addi  7668  mulap0i  7802  divap0i  7904  divmuldivapi  7916  divmul13api  7917  divadddivapi  7918  divdivdivapi  7919  8th4div3  8306  iap0  8310  fldiv4p1lem1div2  9376  sqrt2gt1lt2  10062  abs3lemi  10170  3dvds2dec  10399  flodddiv4  10467  nprmi  10639