Theorem simpl2l 1245

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1105

This theorem is used by:  soisores  7325  frrlem4  8282  omopth2  8565  ttrcltr  9681  fin23lem11  10305  dedekind  11377  xaddass  13279  swrdsbslen  14707  swrdspsleq  14708  ntrivcvgmul  15961  pockthg  16970  gsumsgrpccat  18903  efgred  19822  decpmatmullem  22937  decpmatmul  22938  unconn  23595  basqtop  23877  utop2nei  24416  ucncn  24450  cxple2  26871  cxple2a  26873  nogesgn1ores  27847  nolt02o  27868  nogt01o  27869  nosupbnd1lem1  27881  nosupbnd1lem3  27883  nosupbnd1lem4  27884  nosupbnd1lem5  27885  noinfbnd1lem1  27896  noinfbnd1lem3  27898  noinfbnd1lem4  27899  noinfbnd1lem5  27900  noetalem1  27914  cofcut1  28122  bdayfinbndlem1  28669  ax5seglem1  29287  ax5seglem2  29288  axpasch  29300  axcontlem4  29326  1pthon2v  30513  mhmimasplusg  33366  cvmlift2lem10  35812  br4  36258  cgrcomim  36489  btwnintr  36519  btwnouttr2  36522  btwndiff  36527  btwnconn1lem14  36600  btwnconn3  36603  segcon2  36605  brsegle  36608  brsegle2  36609  segleantisym  36615  seglelin  36616  outsideofeu  36631  eqlkr  39901  eqlkr2  39902  lkrlsp  39904  atbtwn  40248  athgt  40258  3dimlem3  40263  3dimlem3OLDN  40264  3dim3  40271  3atlem7  40291  4atlem0a  40395  4atlem3a  40399  4atlem11  40411  lneq2at  40580  lnatexN  40581  cdlemb  40596  paddasslem6  40627  llnexchb2  40671  lhp2lt  40803  lhpexle2lem  40811  lhpexle3  40814  lhpmcvr3  40827  lhpat3  40848  ltrnnidn  40976  ltrneq3  41010  cdleme17b  41089  cdleme25a  41155  cdleme25dN  41158  cdleme27cl  41168  cdlemefrs29bpre0  41198  cdlemefs32sn1aw  41216  cdleme32le  41249  cdleme46f2g2  41295  cdleme46f2g1  41296  cdleme50trn3  41355  trlord  41371  ltrniotavalbN  41386  cdlemg6  41425  cdlemg7N  41428  cdlemg11b  41444  cdlemg15a  41457  cdlemg15  41458  cdlemg39  41518  trlcone  41530  cdlemg42  41531  tendoconid  41631  tendotr  41632  cdlemk39u  41770  cdlemk19u  41772  cdleml5N  41782  cdlemm10N  41920  dihord11b  42024  dihord2pre  42027  dihvalcqpre  42037  dihopelvalcpre  42050  dihord6apre  42058  dihord4  42060  dihord5b  42061  dihglblem5apreN  42093  dihmeetlem13N  42121  dihmeetlem19N  42127  dih1dimatlem0  42130  qirropth  43663  mzpcong  43727  jm2.25lem1  43753  jm2.26  43757  idomsubgmo  43948  fourierdlem42  46891  fourierdlem97  46945  clnbgrgrimlem  48726  line2  49560  itscnhlinecirc02plem2  49591