Theorem simpl21 1251

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  frrlem10  8336  nosupbnd2lem1  27778  noinfbnd2lem1  27793  brbtwn2  28938  ax5seglem3a  28963  ax5seg  28971  axpasch  28974  axeuclid  28996  br8d  32632  br8  35718  cgrextend  35972  segconeq  35974  trisegint  35992  ifscgr  36008  cgrsub  36009  cgrxfr  36019  lineext  36040  seglecgr12im  36074  segletr  36078  lineunray  36111  lineelsb2  36112  cvrcmp  39239  cvlatexch3  39294  cvlsupr2  39299  atexchcvrN  39397  3dim1  39424  3dim2  39425  ps-1  39434  ps-2  39435  3atlem3  39442  3atlem5  39444  lplnnle2at  39498  lplnllnneN  39513  2llnjaN  39523  4atlem3  39553  4atlem10b  39562  4atlem12  39569  2llnma3r  39745  paddasslem4  39780  paddasslem7  39783  paddasslem8  39784  paddasslem12  39788  paddasslem13  39789  pmodlem1  39803  pmodlem2  39804  llnexchb2lem  39825  4atex2  40034  ltrnatlw  40140  trlval4  40145  arglem1N  40147  cdlemd4  40158  cdlemd5  40159  cdleme0moN  40182  cdleme16  40242  cdleme20  40281  cdleme21j  40293  cdleme21k  40295  cdleme27N  40326  cdleme28c  40329  cdleme43fsv1snlem  40377  cdleme38n  40421  cdleme40n  40425  cdleme41snaw  40433  cdlemg6c  40577  cdlemg8c  40586  cdlemg8  40588  cdlemg12e  40604  cdlemg16  40614  cdlemg16ALTN  40615  cdlemg16z  40616  cdlemg16zz  40617  cdlemg18a  40635  cdlemg20  40642  cdlemg22  40644  cdlemg37  40646  cdlemg27b  40653  cdlemg31d  40657  cdlemg33  40668  cdlemg38  40672  cdlemg44b  40689  cdlemk38  40872  cdlemk35s-id  40895  cdlemk39s-id  40897  cdlemk55  40918  cdlemk35u  40921  cdlemk55u  40923  cdleml3N  40935  cdlemn11pre  41167