Theorem 3adant3r 1224

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)

Hypothesis

Ref	Expression
3adant1l.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3adant3r	⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃)

Proof of Theorem 3adant3r

Step	Hyp	Ref	Expression
1		3adant1l.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3com13 1197	. . 3 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃)
3	2	3adant1r 1220	. 2 ⊢ (((𝜒 ∧ 𝜏) ∧ 𝜓 ∧ 𝜑) → 𝜃)
4	3	3com13 1197	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 967

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

This theorem depends on definitions:  df-bi 116  df-3an 969

This theorem is referenced by:  addassnqg  7314  mulassnqg  7316  prarloc  7435  ltpopr  7527  ltexprlemfl  7541  ltexprlemfu  7543  addasssrg  7688  axaddass  7804  apmul1  8675  ltmul2  8742  lemul2  8743  dvdscmulr  11746  dvdsmulcr  11747  modremain  11851  ndvdsadd  11853  rpexp12i  12064  xblcntrps  12954  xblcntr  12955