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 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  soisores  7283  frrlem4  8241  omopth2  8521  ttrcltr  9637  fin23lem11  10239  dedekind  11308  xaddass  13176  swrdsbslen  14600  swrdspsleq  14601  ntrivcvgmul  15837  pockthg  16846  gsumsgrpccat  18777  efgred  19689  decpmatmullem  22727  decpmatmul  22728  unconn  23385  basqtop  23667  utop2nei  24206  ucncn  24240  cxple2  26674  cxple2a  26676  nogesgn1ores  27654  nolt02o  27675  nogt01o  27676  nosupbnd1lem1  27688  nosupbnd1lem3  27690  nosupbnd1lem4  27691  nosupbnd1lem5  27692  noinfbnd1lem1  27703  noinfbnd1lem3  27705  noinfbnd1lem4  27706  noinfbnd1lem5  27707  noetalem1  27721  cofcut1  27928  bdayfinbndlem1  28475  ax5seglem1  29013  ax5seglem2  29014  axpasch  29026  axcontlem4  29052  1pthon2v  30240  mhmimasplusg  33130  cvmlift2lem10  35525  br4  35971  cgrcomim  36202  btwnintr  36232  btwnouttr2  36235  btwndiff  36240  btwnconn1lem14  36313  btwnconn3  36316  segcon2  36318  brsegle  36321  brsegle2  36322  segleantisym  36328  seglelin  36329  outsideofeu  36344  eqlkr  39469  eqlkr2  39470  lkrlsp  39472  atbtwn  39816  athgt  39826  3dimlem3  39831  3dimlem3OLDN  39832  3dim3  39839  3atlem7  39859  4atlem0a  39963  4atlem3a  39967  4atlem11  39979  lneq2at  40148  lnatexN  40149  cdlemb  40164  paddasslem6  40195  llnexchb2  40239  lhp2lt  40371  lhpexle2lem  40379  lhpexle3  40382  lhpmcvr3  40395  lhpat3  40416  ltrnnidn  40544  ltrneq3  40578  cdleme17b  40657  cdleme25a  40723  cdleme25dN  40726  cdleme27cl  40736  cdlemefrs29bpre0  40766  cdlemefs32sn1aw  40784  cdleme32le  40817  cdleme46f2g2  40863  cdleme46f2g1  40864  cdleme50trn3  40923  trlord  40939  ltrniotavalbN  40954  cdlemg6  40993  cdlemg7N  40996  cdlemg11b  41012  cdlemg15a  41025  cdlemg15  41026  cdlemg39  41086  trlcone  41098  cdlemg42  41099  tendoconid  41199  tendotr  41200  cdlemk39u  41338  cdlemk19u  41340  cdleml5N  41350  cdlemm10N  41488  dihord11b  41592  dihord2pre  41595  dihvalcqpre  41605  dihopelvalcpre  41618  dihord6apre  41626  dihord4  41628  dihord5b  41629  dihglblem5apreN  41661  dihmeetlem13N  41689  dihmeetlem19N  41695  dih1dimatlem0  41698  qirropth  43259  mzpcong  43323  jm2.25lem1  43349  jm2.26  43353  idomsubgmo  43544  fourierdlem42  46501  fourierdlem97  46555  clnbgrgrimlem  48287  line2  49106  itscnhlinecirc02plem2  49137