Theorem simpl11 1129

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

Assertion

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

Proof of Theorem simpl11

Step	Hyp	Ref	Expression
1		simp11 1084	. 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  tsmsxp  21768  brbtwn2  25585  ax5seg  25618  br8  30899  btwndiff  31304  ifscgr  31321  seglecgr12im  31387  lkrshp  33410  cvlcvr1  33644  atbtwn  33750  3dimlem3  33765  3dimlem3OLDN  33766  1cvratex  33777  llnmlplnN  33843  4atlem3  33900  4atlem3a  33901  4atlem11  33913  4atlem12  33916  lnatexN  34083  cdlemb  34098  paddasslem4  34127  paddasslem10  34133  pmodlem1  34150  llnexchb2lem  34172  llnexchb2  34173  arglem1N  34495  cdlemd4  34506  cdlemd9  34511  cdlemd  34512  cdleme16  34590  cdleme20  34630  cdleme21i  34641  cdleme21k  34644  cdleme27N  34675  cdleme28c  34678  cdlemefrs29bpre0  34702  cdlemefrs29clN  34705  cdlemefrs32fva  34706  cdleme41sn3a  34739  cdleme32fva  34743  cdleme40n  34774  cdlemg12e  34953  cdlemg15a  34961  cdlemg15  34962  cdlemg16ALTN  34964  cdlemg16z  34965  cdlemg20  34991  cdlemg22  34993  cdlemg29  35011  cdlemg38  35021  cdlemk33N  35215  cdlemk56  35277  dihord11b  35529  dihord2pre  35532  dihord4  35565  fourierdlem77  39076  3vfriswmgr  41448