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  7626  m1p1sr  7980  m1m1sr  7981  0lt1sr  7985  axi2m1  8095  mul4i  8327  add4i  8344  addsub4i  8475  muladdi  8588  lt2addi  8690  le2addi  8691  mulap0i  8836  divap0i  8940  divmuldivapi  8952  divmul13api  8953  divadddivapi  8954  divdivdivapi  8955  subrecapi  9020  8th4div3  9363  iap0  9367  fldiv4p1lem1div2  10566  sqrt2gt1lt2  11614  abs3lemi  11722  3dvds2dec  12432  flodddiv4  12502  nprmi  12701  modxai  12994  sinhalfpilem  15521  cos0pilt1  15582  lgsdir2lem1  15763  lgsdir2lem5  15767  m1lgs  15820  2lgslem4  15838