Theorem simpl21 1247

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  brbtwn2  26690  ax5seglem3a  26715  ax5seg  26723  axpasch  26726  axeuclid  26748  br8d  30360  br8  32992  frrlem10  33132  nosupbnd2lem1  33215  cgrextend  33469  segconeq  33471  trisegint  33489  ifscgr  33505  cgrsub  33506  cgrxfr  33516  lineext  33537  seglecgr12im  33571  segletr  33575  lineunray  33608  lineelsb2  33609  cvrcmp  36418  cvlatexch3  36473  cvlsupr2  36478  atexchcvrN  36575  3dim1  36602  3dim2  36603  ps-1  36612  ps-2  36613  3atlem3  36620  3atlem5  36622  lplnnle2at  36676  lplnllnneN  36691  2llnjaN  36701  4atlem3  36731  4atlem10b  36740  4atlem12  36747  2llnma3r  36923  paddasslem4  36958  paddasslem7  36961  paddasslem8  36962  paddasslem12  36966  paddasslem13  36967  pmodlem1  36981  pmodlem2  36982  llnexchb2lem  37003  4atex2  37212  ltrnatlw  37318  trlval4  37323  arglem1N  37325  cdlemd4  37336  cdlemd5  37337  cdleme0moN  37360  cdleme16  37420  cdleme20  37459  cdleme21j  37471  cdleme21k  37473  cdleme27N  37504  cdleme28c  37507  cdleme43fsv1snlem  37555  cdleme38n  37599  cdleme40n  37603  cdleme41snaw  37611  cdlemg6c  37755  cdlemg8c  37764  cdlemg8  37766  cdlemg12e  37782  cdlemg16  37792  cdlemg16ALTN  37793  cdlemg16z  37794  cdlemg16zz  37795  cdlemg18a  37813  cdlemg20  37820  cdlemg22  37822  cdlemg37  37824  cdlemg27b  37831  cdlemg31d  37835  cdlemg33  37846  cdlemg38  37850  cdlemg44b  37867  cdlemk38  38050  cdlemk35s-id  38073  cdlemk39s-id  38075  cdlemk55  38096  cdlemk35u  38099  cdlemk55u  38101  cdleml3N  38113  cdlemn11pre  38345