Theorem simpl21 1268

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 1208	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜑)
2	1	3ad2antl2 1203	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  frrlem10  8294  nosupbnd2lem1  27847  noinfbnd2lem1  27862  brbtwn2  29198  ax5seglem3a  29223  ax5seg  29231  axpasch  29234  axeuclid  29256  br8d  32896  br8  36183  cgrextend  36435  segconeq  36437  trisegint  36455  ifscgr  36471  cgrsub  36472  cgrxfr  36482  lineext  36503  seglecgr12im  36537  segletr  36541  lineunray  36574  lineelsb2  36575  cvrcmp  39984  cvlatexch3  40039  cvlsupr2  40044  atexchcvrN  40141  3dim1  40168  3dim2  40169  ps-1  40178  ps-2  40179  3atlem3  40186  3atlem5  40188  lplnnle2at  40242  lplnllnneN  40257  2llnjaN  40267  4atlem3  40297  4atlem10b  40306  4atlem12  40313  2llnma3r  40489  paddasslem4  40524  paddasslem7  40527  paddasslem8  40528  paddasslem12  40532  paddasslem13  40533  pmodlem1  40547  pmodlem2  40548  llnexchb2lem  40569  4atex2  40778  ltrnatlw  40884  trlval4  40889  arglem1N  40891  cdlemd4  40902  cdlemd5  40903  cdleme0moN  40926  cdleme16  40986  cdleme20  41025  cdleme21j  41037  cdleme21k  41039  cdleme27N  41070  cdleme28c  41073  cdleme43fsv1snlem  41121  cdleme38n  41165  cdleme40n  41169  cdleme41snaw  41177  cdlemg6c  41321  cdlemg8c  41330  cdlemg8  41332  cdlemg12e  41348  cdlemg16  41358  cdlemg16ALTN  41359  cdlemg16z  41360  cdlemg16zz  41361  cdlemg18a  41379  cdlemg20  41386  cdlemg22  41388  cdlemg37  41390  cdlemg27b  41397  cdlemg31d  41401  cdlemg33  41412  cdlemg38  41416  cdlemg44b  41433  cdlemk38  41616  cdlemk35s-id  41639  cdlemk39s-id  41641  cdlemk55  41662  cdlemk35u  41665  cdlemk55u  41667  cdleml3N  41679  cdlemn11pre  41911