Theorem simpl21 1132

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

Assertion

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

Proof of Theorem simpl21

Step	Hyp	Ref	Expression
1		simp21 1087	. 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:  brbtwn2  25585  ax5seglem3a  25610  ax5seg  25618  axpasch  25621  axeuclid  25643  br8d  28802  br8  30899  cgrextend  31285  segconeq  31287  trisegint  31305  ifscgr  31321  cgrsub  31322  cgrxfr  31332  lineext  31353  seglecgr12im  31387  segletr  31391  lineunray  31424  lineelsb2  31425  cvrcmp  33588  cvlatexch3  33643  cvlsupr2  33648  atexchcvrN  33744  3dim1  33771  3dim2  33772  ps-1  33781  ps-2  33782  3atlem3  33789  3atlem5  33791  lplnnle2at  33845  lplnllnneN  33860  2llnjaN  33870  4atlem3  33900  4atlem10b  33909  4atlem12  33916  2llnma3r  34092  paddasslem4  34127  paddasslem7  34130  paddasslem8  34131  paddasslem12  34135  paddasslem13  34136  pmodlem1  34150  pmodlem2  34151  llnexchb2lem  34172  4atex2  34381  ltrnatlw  34488  trlval4  34493  arglem1N  34495  cdlemd4  34506  cdlemd5  34507  cdleme0moN  34530  cdleme16  34590  cdleme20  34630  cdleme21j  34642  cdleme21k  34644  cdleme27N  34675  cdleme28c  34678  cdleme43fsv1snlem  34726  cdleme38n  34770  cdleme40n  34774  cdleme41snaw  34782  cdlemg6c  34926  cdlemg8c  34935  cdlemg8  34937  cdlemg12e  34953  cdlemg16  34963  cdlemg16ALTN  34964  cdlemg16z  34965  cdlemg16zz  34966  cdlemg18a  34984  cdlemg20  34991  cdlemg22  34993  cdlemg37  34995  cdlemg27b  35002  cdlemg31d  35006  cdlemg33  35017  cdlemg38  35021  cdlemg44b  35038  cdlemk38  35221  cdlemk35s-id  35244  cdlemk39s-id  35246  cdlemk55  35267  cdlemk35u  35270  cdlemk55u  35272  cdleml3N  35284  cdlemn11pre  35517