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  7282  frrlem4  8239  omopth2  8519  ttrcltr  9637  fin23lem11  10239  dedekind  11309  xaddass  13201  swrdsbslen  14627  swrdspsleq  14628  ntrivcvgmul  15867  pockthg  16877  gsumsgrpccat  18808  efgred  19723  decpmatmullem  22736  decpmatmul  22737  unconn  23394  basqtop  23676  utop2nei  24215  ucncn  24249  cxple2  26661  cxple2a  26663  nogesgn1ores  27638  nolt02o  27659  nogt01o  27660  nosupbnd1lem1  27672  nosupbnd1lem3  27674  nosupbnd1lem4  27675  nosupbnd1lem5  27676  noinfbnd1lem1  27687  noinfbnd1lem3  27689  noinfbnd1lem4  27690  noinfbnd1lem5  27691  noetalem1  27705  cofcut1  27912  bdayfinbndlem1  28459  ax5seglem1  28997  ax5seglem2  28998  axpasch  29010  axcontlem4  29036  1pthon2v  30223  mhmimasplusg  33098  cvmlift2lem10  35494  br4  35940  cgrcomim  36171  btwnintr  36201  btwnouttr2  36204  btwndiff  36209  btwnconn1lem14  36282  btwnconn3  36285  segcon2  36287  brsegle  36290  brsegle2  36291  segleantisym  36297  seglelin  36298  outsideofeu  36313  eqlkr  39545  eqlkr2  39546  lkrlsp  39548  atbtwn  39892  athgt  39902  3dimlem3  39907  3dimlem3OLDN  39908  3dim3  39915  3atlem7  39935  4atlem0a  40039  4atlem3a  40043  4atlem11  40055  lneq2at  40224  lnatexN  40225  cdlemb  40240  paddasslem6  40271  llnexchb2  40315  lhp2lt  40447  lhpexle2lem  40455  lhpexle3  40458  lhpmcvr3  40471  lhpat3  40492  ltrnnidn  40620  ltrneq3  40654  cdleme17b  40733  cdleme25a  40799  cdleme25dN  40802  cdleme27cl  40812  cdlemefrs29bpre0  40842  cdlemefs32sn1aw  40860  cdleme32le  40893  cdleme46f2g2  40939  cdleme46f2g1  40940  cdleme50trn3  40999  trlord  41015  ltrniotavalbN  41030  cdlemg6  41069  cdlemg7N  41072  cdlemg11b  41088  cdlemg15a  41101  cdlemg15  41102  cdlemg39  41162  trlcone  41174  cdlemg42  41175  tendoconid  41275  tendotr  41276  cdlemk39u  41414  cdlemk19u  41416  cdleml5N  41426  cdlemm10N  41564  dihord11b  41668  dihord2pre  41671  dihvalcqpre  41681  dihopelvalcpre  41694  dihord6apre  41702  dihord4  41704  dihord5b  41705  dihglblem5apreN  41737  dihmeetlem13N  41765  dihmeetlem19N  41771  dih1dimatlem0  41774  qirropth  43336  mzpcong  43400  jm2.25lem1  43426  jm2.26  43430  idomsubgmo  43621  fourierdlem42  46577  fourierdlem97  46631  clnbgrgrimlem  48409  line2  49228  itscnhlinecirc02plem2  49259