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  8301  nosupbnd2lem1  27916  noinfbnd2lem1  27931  brbtwn2  29292  ax5seglem3a  29317  ax5seg  29325  axpasch  29328  axeuclid  29350  br8d  32990  br8  36269  cgrextend  36521  segconeq  36523  trisegint  36541  ifscgr  36557  cgrsub  36558  cgrxfr  36568  lineext  36589  seglecgr12im  36623  segletr  36627  lineunray  36660  lineelsb2  36661  cvrcmp  40098  cvlatexch3  40153  cvlsupr2  40158  atexchcvrN  40255  3dim1  40282  3dim2  40283  ps-1  40292  ps-2  40293  3atlem3  40300  3atlem5  40302  lplnnle2at  40356  lplnllnneN  40371  2llnjaN  40381  4atlem3  40411  4atlem10b  40420  4atlem12  40427  2llnma3r  40603  paddasslem4  40638  paddasslem7  40641  paddasslem8  40642  paddasslem12  40646  paddasslem13  40647  pmodlem1  40661  pmodlem2  40662  llnexchb2lem  40683  4atex2  40892  ltrnatlw  40998  trlval4  41003  arglem1N  41005  cdlemd4  41016  cdlemd5  41017  cdleme0moN  41040  cdleme16  41100  cdleme20  41139  cdleme21j  41151  cdleme21k  41153  cdleme27N  41184  cdleme28c  41187  cdleme43fsv1snlem  41235  cdleme38n  41279  cdleme40n  41283  cdleme41snaw  41291  cdlemg6c  41435  cdlemg8c  41444  cdlemg8  41446  cdlemg12e  41462  cdlemg16  41472  cdlemg16ALTN  41473  cdlemg16z  41474  cdlemg16zz  41475  cdlemg18a  41493  cdlemg20  41500  cdlemg22  41502  cdlemg37  41504  cdlemg27b  41511  cdlemg31d  41515  cdlemg33  41526  cdlemg38  41530  cdlemg44b  41547  cdlemk38  41730  cdlemk35s-id  41753  cdlemk39s-id  41755  cdlemk55  41776  cdlemk35u  41779  cdlemk55u  41781  cdleml3N  41793  cdlemn11pre  42025