Theorem simpl12 1130

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

Assertion

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

Proof of Theorem simpl12

Step	Hyp	Ref	Expression
1		simp12 1085	. 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  pmatcollpw1lem1  20398  pmatcollpw1  20400  mp2pm2mplem2  20431  brbtwn2  25585  ax5seg  25618  br8  30899  ifscgr  31321  seglecgr12im  31387  lkrshp  33410  atlatle  33625  cvlcvr1  33644  atbtwn  33750  3dimlem3  33765  3dimlem3OLDN  33766  1cvratex  33777  llnmlplnN  33843  4atlem3  33900  4atlem3a  33901  4atlem11  33913  4atlem12  33916  cdlemb  34098  paddasslem4  34127  paddasslem10  34133  pmodlem1  34150  llnexchb2lem  34172  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  cdlemk33N  35215  cdlemk56  35277  fourierdlem77  39076  3vfriswmgr  41448