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  7625  m1p1sr  7979  m1m1sr  7980  0lt1sr  7984  axi2m1  8094  mul4i  8326  add4i  8343  addsub4i  8474  muladdi  8587  lt2addi  8689  le2addi  8690  mulap0i  8835  divap0i  8939  divmuldivapi  8951  divmul13api  8952  divadddivapi  8953  divdivdivapi  8954  subrecapi  9019  8th4div3  9362  iap0  9366  fldiv4p1lem1div2  10564  sqrt2gt1lt2  11609  abs3lemi  11717  3dvds2dec  12426  flodddiv4  12496  nprmi  12695  modxai  12988  sinhalfpilem  15514  cos0pilt1  15575  lgsdir2lem1  15756  lgsdir2lem5  15760  m1lgs  15813  2lgslem4  15831