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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ 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 402  df-3an 1105

This theorem is used by:  soisores  7358  frrlem4  8335  omopth2  8620  ttrcltr  9744  fin23lem11  10422  dedekind  11500  xaddass  13406  swrdsbslen  14842  swrdspsleq  14843  ntrivcvgmul  16100  pockthg  17113  gsumsgrpccat  19065  efgred  19992  decpmatmullem  23119  decpmatmul  23120  unconn  23777  basqtop  24060  utop2nei  24599  ucncn  24633  cxple2  27055  cxple2a  27057  nogesgn1ores  28061  nolt02o  28082  nogt01o  28083  nosupbnd1lem1  28095  nosupbnd1lem3  28097  nosupbnd1lem4  28098  nosupbnd1lem5  28099  noinfbnd1lem1  28110  noinfbnd1lem3  28112  noinfbnd1lem4  28113  noinfbnd1lem5  28114  noetalem1  28128  cofcut1  28336  bdayfinbndlem1  28883  ax5seglem1  29536  ax5seglem2  29537  axpasch  29549  axcontlem4  29575  1pthon2v  30784  mhmimasplusg  33668  cvmlift2lem10  36244  br4  36701  cgrcomim  36932  btwnintr  36962  btwnouttr2  36965  btwndiff  36970  btwnconn1lem14  37043  btwnconn3  37046  segcon2  37048  brsegle  37051  brsegle2  37052  segleantisym  37058  seglelin  37059  outsideofeu  37074  eqlkr  40348  eqlkr2  40349  lkrlsp  40351  atbtwn  40695  athgt  40705  3dimlem3  40710  3dimlem3OLDN  40711  3dim3  40718  3atlem7  40738  4atlem0a  40842  4atlem3a  40846  4atlem11  40858  lneq2at  41027  lnatexN  41028  cdlemb  41043  paddasslem6  41074  llnexchb2  41118  lhp2lt  41250  lhpexle2lem  41258  lhpexle3  41261  lhpmcvr3  41274  lhpat3  41295  ltrnnidn  41423  ltrneq3  41457  cdleme17b  41536  cdleme25a  41602  cdleme25dN  41605  cdleme27cl  41615  cdlemefrs29bpre0  41645  cdlemefs32sn1aw  41663  cdleme32le  41696  cdleme46f2g2  41742  cdleme46f2g1  41743  cdleme50trn3  41802  trlord  41818  ltrniotavalbN  41833  cdlemg6  41872  cdlemg7N  41875  cdlemg11b  41891  cdlemg15a  41904  cdlemg15  41905  cdlemg39  41965  trlcone  41977  cdlemg42  41978  tendoconid  42078  tendotr  42079  cdlemk39u  42217  cdlemk19u  42219  cdleml5N  42229  cdlemm10N  42367  dihord11b  42471  dihord2pre  42474  dihvalcqpre  42484  dihopelvalcpre  42497  dihord6apre  42505  dihord4  42507  dihord5b  42508  dihglblem5apreN  42540  dihmeetlem13N  42568  dihmeetlem19N  42574  dih1dimatlem0  42577  qirropth  44108  mzpcong  44172  jm2.25lem1  44198  jm2.26  44202  idomsubgmo  44387  fourierdlem42  47364  fourierdlem97  47418  clnbgrgrimlem  49236  line2  50069  itscnhlinecirc02plem2  50100