Theorem simpl21 1264

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  frrlem10  8271  nosupbnd2lem1  27756  noinfbnd2lem1  27771  brbtwn2  29052  ax5seglem3a  29077  ax5seg  29085  axpasch  29088  axeuclid  29110  br8d  32760  br8  36070  cgrextend  36322  segconeq  36324  trisegint  36342  ifscgr  36358  cgrsub  36359  cgrxfr  36369  lineext  36390  seglecgr12im  36424  segletr  36428  lineunray  36461  lineelsb2  36462  cvrcmp  39871  cvlatexch3  39926  cvlsupr2  39931  atexchcvrN  40028  3dim1  40055  3dim2  40056  ps-1  40065  ps-2  40066  3atlem3  40073  3atlem5  40075  lplnnle2at  40129  lplnllnneN  40144  2llnjaN  40154  4atlem3  40184  4atlem10b  40193  4atlem12  40200  2llnma3r  40376  paddasslem4  40411  paddasslem7  40414  paddasslem8  40415  paddasslem12  40419  paddasslem13  40420  pmodlem1  40434  pmodlem2  40435  llnexchb2lem  40456  4atex2  40665  ltrnatlw  40771  trlval4  40776  arglem1N  40778  cdlemd4  40789  cdlemd5  40790  cdleme0moN  40813  cdleme16  40873  cdleme20  40912  cdleme21j  40924  cdleme21k  40926  cdleme27N  40957  cdleme28c  40960  cdleme43fsv1snlem  41008  cdleme38n  41052  cdleme40n  41056  cdleme41snaw  41064  cdlemg6c  41208  cdlemg8c  41217  cdlemg8  41219  cdlemg12e  41235  cdlemg16  41245  cdlemg16ALTN  41246  cdlemg16z  41247  cdlemg16zz  41248  cdlemg18a  41266  cdlemg20  41273  cdlemg22  41275  cdlemg37  41277  cdlemg27b  41284  cdlemg31d  41288  cdlemg33  41299  cdlemg38  41303  cdlemg44b  41320  cdlemk38  41503  cdlemk35s-id  41526  cdlemk39s-id  41528  cdlemk55  41549  cdlemk35u  41552  cdlemk55u  41554  cdleml3N  41566  cdlemn11pre  41798