Theorem simpl21 1270

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

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

Proof of Theorem simpl21

Step	Hyp	Ref	Expression
1		simpl1 1210	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜑)
2	1	3ad2antl2 1205	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  frrlem10  8297  nosupbnd2lem1  28054  noinfbnd2lem1  28069  brbtwn2  29465  ax5seglem3a  29490  ax5seg  29498  axpasch  29501  axeuclid  29523  br8d  33184  br8  36490  cgrextend  36743  segconeq  36745  trisegint  36763  ifscgr  36779  cgrsub  36780  cgrxfr  36790  lineext  36811  seglecgr12im  36845  segletr  36849  lineunray  36882  lineelsb2  36883  cvrcmp  40308  cvlatexch3  40363  cvlsupr2  40368  atexchcvrN  40465  3dim1  40492  3dim2  40493  ps-1  40502  ps-2  40503  3atlem3  40510  3atlem5  40512  lplnnle2at  40566  lplnllnneN  40581  2llnjaN  40591  4atlem3  40621  4atlem10b  40630  4atlem12  40637  2llnma3r  40813  paddasslem4  40848  paddasslem7  40851  paddasslem8  40852  paddasslem12  40856  paddasslem13  40857  pmodlem1  40871  pmodlem2  40872  llnexchb2lem  40893  4atex2  41102  ltrnatlw  41208  trlval4  41213  arglem1N  41215  cdlemd4  41226  cdlemd5  41227  cdleme0moN  41250  cdleme16  41310  cdleme20  41349  cdleme21j  41361  cdleme21k  41363  cdleme27N  41394  cdleme28c  41397  cdleme43fsv1snlem  41445  cdleme38n  41489  cdleme40n  41493  cdleme41snaw  41501  cdlemg6c  41645  cdlemg8c  41654  cdlemg8  41656  cdlemg12e  41672  cdlemg16  41682  cdlemg16ALTN  41683  cdlemg16z  41684  cdlemg16zz  41685  cdlemg18a  41703  cdlemg20  41710  cdlemg22  41712  cdlemg37  41714  cdlemg27b  41721  cdlemg31d  41725  cdlemg33  41736  cdlemg38  41740  cdlemg44b  41757  cdlemk38  41940  cdlemk35s-id  41963  cdlemk39s-id  41965  cdlemk55  41986  cdlemk35u  41989  cdlemk55u  41991  cdleml3N  42003  cdlemn11pre  42235