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 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜑)

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

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 1105

This theorem is referenced by:  frrlem10  8293  nosupbnd2lem1  27857  noinfbnd2lem1  27872  brbtwn2  29233  ax5seglem3a  29258  ax5seg  29266  axpasch  29269  axeuclid  29291  br8d  32931  br8  36226  cgrextend  36478  segconeq  36480  trisegint  36498  ifscgr  36514  cgrsub  36515  cgrxfr  36525  lineext  36546  seglecgr12im  36580  segletr  36584  lineunray  36617  lineelsb2  36618  cvrcmp  40035  cvlatexch3  40090  cvlsupr2  40095  atexchcvrN  40192  3dim1  40219  3dim2  40220  ps-1  40229  ps-2  40230  3atlem3  40237  3atlem5  40239  lplnnle2at  40293  lplnllnneN  40308  2llnjaN  40318  4atlem3  40348  4atlem10b  40357  4atlem12  40364  2llnma3r  40540  paddasslem4  40575  paddasslem7  40578  paddasslem8  40579  paddasslem12  40583  paddasslem13  40584  pmodlem1  40598  pmodlem2  40599  llnexchb2lem  40620  4atex2  40829  ltrnatlw  40935  trlval4  40940  arglem1N  40942  cdlemd4  40953  cdlemd5  40954  cdleme0moN  40977  cdleme16  41037  cdleme20  41076  cdleme21j  41088  cdleme21k  41090  cdleme27N  41121  cdleme28c  41124  cdleme43fsv1snlem  41172  cdleme38n  41216  cdleme40n  41220  cdleme41snaw  41228  cdlemg6c  41372  cdlemg8c  41381  cdlemg8  41383  cdlemg12e  41399  cdlemg16  41409  cdlemg16ALTN  41410  cdlemg16z  41411  cdlemg16zz  41412  cdlemg18a  41430  cdlemg20  41437  cdlemg22  41439  cdlemg37  41441  cdlemg27b  41448  cdlemg31d  41452  cdlemg33  41463  cdlemg38  41467  cdlemg44b  41484  cdlemk38  41667  cdlemk35s-id  41690  cdlemk39s-id  41692  cdlemk55  41713  cdlemk35u  41716  cdlemk55u  41718  cdleml3N  41730  cdlemn11pre  41962