Theorem simpl2l 1243

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 1203	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  soisores  7315  frrlem4  8274  omopth2  8557  ttrcltr  9673  fin23lem11  10289  dedekind  11361  xaddass  13266  swrdsbslen  14692  swrdspsleq  14693  ntrivcvgmul  15946  pockthg  16956  gsumsgrpccat  18889  efgred  19809  decpmatmullem  22889  decpmatmul  22890  unconn  23547  basqtop  23829  utop2nei  24368  ucncn  24402  cxple2  26820  cxple2a  26822  nogesgn1ores  27796  nolt02o  27817  nogt01o  27818  nosupbnd1lem1  27830  nosupbnd1lem3  27832  nosupbnd1lem4  27833  nosupbnd1lem5  27834  noinfbnd1lem1  27845  noinfbnd1lem3  27847  noinfbnd1lem4  27848  noinfbnd1lem5  27849  noetalem1  27863  cofcut1  28071  bdayfinbndlem1  28618  ax5seglem1  29187  ax5seglem2  29188  axpasch  29200  axcontlem4  29226  1pthon2v  30413  mhmimasplusg  33270  cvmlift2lem10  35675  br4  36121  cgrcomim  36352  btwnintr  36382  btwnouttr2  36385  btwndiff  36390  btwnconn1lem14  36463  btwnconn3  36466  segcon2  36468  brsegle  36471  brsegle2  36472  segleantisym  36478  seglelin  36479  outsideofeu  36494  eqlkr  39735  eqlkr2  39736  lkrlsp  39738  atbtwn  40082  athgt  40092  3dimlem3  40097  3dimlem3OLDN  40098  3dim3  40105  3atlem7  40125  4atlem0a  40229  4atlem3a  40233  4atlem11  40245  lneq2at  40414  lnatexN  40415  cdlemb  40430  paddasslem6  40461  llnexchb2  40505  lhp2lt  40637  lhpexle2lem  40645  lhpexle3  40648  lhpmcvr3  40661  lhpat3  40682  ltrnnidn  40810  ltrneq3  40844  cdleme17b  40923  cdleme25a  40989  cdleme25dN  40992  cdleme27cl  41002  cdlemefrs29bpre0  41032  cdlemefs32sn1aw  41050  cdleme32le  41083  cdleme46f2g2  41129  cdleme46f2g1  41130  cdleme50trn3  41189  trlord  41205  ltrniotavalbN  41220  cdlemg6  41259  cdlemg7N  41262  cdlemg11b  41278  cdlemg15a  41291  cdlemg15  41292  cdlemg39  41352  trlcone  41364  cdlemg42  41365  tendoconid  41465  tendotr  41466  cdlemk39u  41604  cdlemk19u  41606  cdleml5N  41616  cdlemm10N  41754  dihord11b  41858  dihord2pre  41861  dihvalcqpre  41871  dihopelvalcpre  41884  dihord6apre  41892  dihord4  41894  dihord5b  41895  dihglblem5apreN  41927  dihmeetlem13N  41955  dihmeetlem19N  41961  dih1dimatlem0  41964  qirropth  43497  mzpcong  43561  jm2.25lem1  43587  jm2.26  43591  idomsubgmo  43782  fourierdlem42  46721  fourierdlem97  46775  clnbgrgrimlem  48553  line2  49383  itscnhlinecirc02plem2  49414