Theorem simp133 1191

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp133	⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜒)

Proof of Theorem simp133

Step	Hyp	Ref	Expression
1		simp33 1092	. 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜒)
2	1	3ad2ant1 1075	1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033

This theorem is referenced by:  tsmsxp  21768  ax5seglem3  25611  exatleN  33708  3atlem1  33787  3atlem2  33788  3atlem6  33792  4atlem11b  33912  4atlem12b  33915  lplncvrlvol2  33919  dalemuea  33935  dath2  34041  4atexlemex6  34378  cdleme22f2  34653  cdleme22g  34654  cdlemg7aN  34931  cdlemg31c  35005  cdlemg36  35020  cdlemj1  35127  cdlemj2  35128  cdlemk23-3  35208  cdlemk26b-3  35211