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  7589  m1p1sr  7943  m1m1sr  7944  0lt1sr  7948  axi2m1  8058  mul4i  8290  add4i  8307  addsub4i  8438  muladdi  8551  lt2addi  8653  le2addi  8654  mulap0i  8799  divap0i  8903  divmuldivapi  8915  divmul13api  8916  divadddivapi  8917  divdivdivapi  8918  subrecapi  8983  8th4div3  9326  iap0  9330  fldiv4p1lem1div2  10520  sqrt2gt1lt2  11555  abs3lemi  11663  3dvds2dec  12372  flodddiv4  12442  nprmi  12641  modxai  12934  sinhalfpilem  15459  cos0pilt1  15520  lgsdir2lem1  15701  lgsdir2lem5  15705  m1lgs  15758  2lgslem4  15776