Theorem mp4an 431

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 430	1 ⊢ 𝜏

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  1lt2nq  7774  m1p1sr  8128  m1m1sr  8129  0lt1sr  8133  axi2m1  8243  mul4i  8476  add4i  8493  addsub4i  8624  muladdi  8738  lt2addi  8840  le2addi  8841  mulap0i  8987  divap0i  9093  divmuldivapi  9105  divmul13api  9106  divadddivapi  9107  divdivdivapi  9108  subrecapi  9173  8th4div3  9529  iap0  9533  fldiv4p1lem1div2  10755  sqrt2gt1lt2  11831  abs3lemi  11940  3dvds2dec  12652  flodddiv4  12722  nprmi  12921  modxai  13218  mod2xnegi  13221  sinhalfpilem  15946  cos0pilt1  16007  log2tlbndlog2  16143  log2ublog2  16147  ppiqub  16216  bposlem8  16241  bposlem9  16242  lgsdir2lem1  16275  lgsdir2lem5  16279  m1lgs  16332  2lgslem4  16350