Theorem simpl2l 1228

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpl2l	⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Proof of Theorem simpl2l

Step	Hyp	Ref	Expression
1		simpll 767	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜑)
2	1	3ad2antl2 1188	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜑)

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

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

This theorem is referenced by:  soisores  7114  frrlem4  8008  omopth2  8290  fin23lem11  9896  dedekind  10960  xaddass  12804  swrdsbslen  14194  swrdspsleq  14195  ntrivcvgmul  15429  pockthg  16422  gsumsgrpccat  18220  efgred  19092  decpmatmullem  21622  decpmatmul  21623  unconn  22280  basqtop  22562  utop2nei  23102  ucncn  23136  cxple2  25539  cxple2a  25541  ax5seglem1  26973  ax5seglem2  26974  axpasch  26986  axcontlem4  27012  1pthon2v  28190  cvmlift2lem10  32941  br4  33395  nogesgn1ores  33563  nolt02o  33584  nogt01o  33585  nosupbnd1lem1  33597  nosupbnd1lem3  33599  nosupbnd1lem4  33600  nosupbnd1lem5  33601  noinfbnd1lem1  33612  noinfbnd1lem3  33614  noinfbnd1lem4  33615  noinfbnd1lem5  33616  noetalem1  33630  cofcut1  33776  cgrcomim  33977  btwnintr  34007  btwnouttr2  34010  btwndiff  34015  btwnconn1lem14  34088  btwnconn3  34091  segcon2  34093  brsegle  34096  brsegle2  34097  segleantisym  34103  seglelin  34104  outsideofeu  34119  eqlkr  36799  eqlkr2  36800  lkrlsp  36802  atbtwn  37146  athgt  37156  3dimlem3  37161  3dimlem3OLDN  37162  3dim3  37169  3atlem7  37189  4atlem0a  37293  4atlem3a  37297  4atlem11  37309  lneq2at  37478  lnatexN  37479  cdlemb  37494  paddasslem6  37525  llnexchb2  37569  lhp2lt  37701  lhpexle2lem  37709  lhpexle3  37712  lhpmcvr3  37725  lhpat3  37746  ltrnnidn  37874  ltrneq3  37908  cdleme17b  37987  cdleme25a  38053  cdleme25dN  38056  cdleme27cl  38066  cdlemefrs29bpre0  38096  cdlemefs32sn1aw  38114  cdleme32le  38147  cdleme46f2g2  38193  cdleme46f2g1  38194  cdleme50trn3  38253  trlord  38269  ltrniotavalbN  38284  cdlemg6  38323  cdlemg7N  38326  cdlemg11b  38342  cdlemg15a  38355  cdlemg15  38356  cdlemg39  38416  trlcone  38428  cdlemg42  38429  tendoconid  38529  tendotr  38530  cdlemk39u  38668  cdlemk19u  38670  cdleml5N  38680  cdlemm10N  38818  dihord11b  38922  dihord2pre  38925  dihvalcqpre  38935  dihopelvalcpre  38948  dihord6apre  38956  dihord4  38958  dihord5b  38959  dihglblem5apreN  38991  dihmeetlem13N  39019  dihmeetlem19N  39025  dih1dimatlem0  39028  qirropth  40374  mzpcong  40438  jm2.25lem1  40464  jm2.26  40468  idomsubgmo  40667  fourierdlem42  43308  fourierdlem97  43362  line2  45714  itscnhlinecirc02plem2  45745