Theorem simpl13 1131

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

Assertion

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

Proof of Theorem simpl13

Step	Hyp	Ref	Expression
1		simp13 1086	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜒)
2	1	adantr 480	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 383   ∧ 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:  pythagtriplem4  15362  mply1topmatcl  20429  brbtwn2  25585  ax5seg  25618  br8  30899  btwndiff  31304  ifscgr  31321  seglecgr12im  31387  atlatle  33625  cvlcvr1  33644  atbtwn  33750  3dimlem3  33765  3dimlem3OLDN  33766  4atlem3  33900  4atlem11  33913  4atlem12  33916  2lplnj  33924  paddasslem4  34127  paddasslem10  34133  pmodlem1  34150  llnexchb2lem  34172  pclfinclN  34254  arglem1N  34495  cdlemd4  34506  cdlemd  34512  cdleme16  34590  cdleme20  34630  cdleme21k  34644  cdleme22cN  34648  cdleme27N  34675  cdleme28c  34678  cdleme29ex  34680  cdleme32fva  34743  cdleme40n  34774  cdlemg15a  34961  cdlemg15  34962  cdlemg16ALTN  34964  cdlemg16z  34965  cdlemg20  34991  cdlemg22  34993  cdlemg29  35011  cdlemg38  35021  cdlemk56  35277  dihord2pre  35532  uzwo4  38246  fourierdlem77  39076