Theorem simpl2l 1227

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

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

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 1088

This theorem is referenced by:  soisores  7261  frrlem4  8219  omopth2  8499  ttrcltr  9606  fin23lem11  10205  dedekind  11273  xaddass  13145  swrdsbslen  14569  swrdspsleq  14570  ntrivcvgmul  15806  pockthg  16815  gsumsgrpccat  18745  efgred  19658  decpmatmullem  22684  decpmatmul  22685  unconn  23342  basqtop  23624  utop2nei  24163  ucncn  24197  cxple2  26631  cxple2a  26633  nogesgn1ores  27611  nolt02o  27632  nogt01o  27633  nosupbnd1lem1  27645  nosupbnd1lem3  27647  nosupbnd1lem4  27648  nosupbnd1lem5  27649  noinfbnd1lem1  27660  noinfbnd1lem3  27662  noinfbnd1lem4  27663  noinfbnd1lem5  27664  noetalem1  27678  cofcut1  27862  ax5seglem1  28904  ax5seglem2  28905  axpasch  28917  axcontlem4  28943  1pthon2v  30128  mhmimasplusg  33014  cvmlift2lem10  35344  br4  35790  cgrcomim  36022  btwnintr  36052  btwnouttr2  36055  btwndiff  36060  btwnconn1lem14  36133  btwnconn3  36136  segcon2  36138  brsegle  36141  brsegle2  36142  segleantisym  36148  seglelin  36149  outsideofeu  36164  eqlkr  39137  eqlkr2  39138  lkrlsp  39140  atbtwn  39484  athgt  39494  3dimlem3  39499  3dimlem3OLDN  39500  3dim3  39507  3atlem7  39527  4atlem0a  39631  4atlem3a  39635  4atlem11  39647  lneq2at  39816  lnatexN  39817  cdlemb  39832  paddasslem6  39863  llnexchb2  39907  lhp2lt  40039  lhpexle2lem  40047  lhpexle3  40050  lhpmcvr3  40063  lhpat3  40084  ltrnnidn  40212  ltrneq3  40246  cdleme17b  40325  cdleme25a  40391  cdleme25dN  40394  cdleme27cl  40404  cdlemefrs29bpre0  40434  cdlemefs32sn1aw  40452  cdleme32le  40485  cdleme46f2g2  40531  cdleme46f2g1  40532  cdleme50trn3  40591  trlord  40607  ltrniotavalbN  40622  cdlemg6  40661  cdlemg7N  40664  cdlemg11b  40680  cdlemg15a  40693  cdlemg15  40694  cdlemg39  40754  trlcone  40766  cdlemg42  40767  tendoconid  40867  tendotr  40868  cdlemk39u  41006  cdlemk19u  41008  cdleml5N  41018  cdlemm10N  41156  dihord11b  41260  dihord2pre  41263  dihvalcqpre  41273  dihopelvalcpre  41286  dihord6apre  41294  dihord4  41296  dihord5b  41297  dihglblem5apreN  41329  dihmeetlem13N  41357  dihmeetlem19N  41363  dih1dimatlem0  41366  qirropth  42940  mzpcong  43004  jm2.25lem1  43030  jm2.26  43034  idomsubgmo  43225  fourierdlem42  46186  fourierdlem97  46240  clnbgrgrimlem  47963  line2  48783  itscnhlinecirc02plem2  48814