Theorem simpl2l 1227

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 1187	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  7347  frrlem4  8314  omopth2  8622  ttrcltr  9756  fin23lem11  10357  dedekind  11424  xaddass  13291  swrdsbslen  14702  swrdspsleq  14703  ntrivcvgmul  15938  pockthg  16944  gsumsgrpccat  18853  efgred  19766  decpmatmullem  22777  decpmatmul  22778  unconn  23437  basqtop  23719  utop2nei  24259  ucncn  24294  cxple2  26739  cxple2a  26741  nogesgn1ores  27719  nolt02o  27740  nogt01o  27741  nosupbnd1lem1  27753  nosupbnd1lem3  27755  nosupbnd1lem4  27756  nosupbnd1lem5  27757  noinfbnd1lem1  27768  noinfbnd1lem3  27770  noinfbnd1lem4  27771  noinfbnd1lem5  27772  noetalem1  27786  cofcut1  27954  ax5seglem1  28943  ax5seglem2  28944  axpasch  28956  axcontlem4  28982  1pthon2v  30172  mhmimasplusg  33043  cvmlift2lem10  35317  br4  35758  cgrcomim  35990  btwnintr  36020  btwnouttr2  36023  btwndiff  36028  btwnconn1lem14  36101  btwnconn3  36104  segcon2  36106  brsegle  36109  brsegle2  36110  segleantisym  36116  seglelin  36117  outsideofeu  36132  eqlkr  39100  eqlkr2  39101  lkrlsp  39103  atbtwn  39448  athgt  39458  3dimlem3  39463  3dimlem3OLDN  39464  3dim3  39471  3atlem7  39491  4atlem0a  39595  4atlem3a  39599  4atlem11  39611  lneq2at  39780  lnatexN  39781  cdlemb  39796  paddasslem6  39827  llnexchb2  39871  lhp2lt  40003  lhpexle2lem  40011  lhpexle3  40014  lhpmcvr3  40027  lhpat3  40048  ltrnnidn  40176  ltrneq3  40210  cdleme17b  40289  cdleme25a  40355  cdleme25dN  40358  cdleme27cl  40368  cdlemefrs29bpre0  40398  cdlemefs32sn1aw  40416  cdleme32le  40449  cdleme46f2g2  40495  cdleme46f2g1  40496  cdleme50trn3  40555  trlord  40571  ltrniotavalbN  40586  cdlemg6  40625  cdlemg7N  40628  cdlemg11b  40644  cdlemg15a  40657  cdlemg15  40658  cdlemg39  40718  trlcone  40730  cdlemg42  40731  tendoconid  40831  tendotr  40832  cdlemk39u  40970  cdlemk19u  40972  cdleml5N  40982  cdlemm10N  41120  dihord11b  41224  dihord2pre  41227  dihvalcqpre  41237  dihopelvalcpre  41250  dihord6apre  41258  dihord4  41260  dihord5b  41261  dihglblem5apreN  41293  dihmeetlem13N  41321  dihmeetlem19N  41327  dih1dimatlem0  41330  qirropth  42919  mzpcong  42984  jm2.25lem1  43010  jm2.26  43014  idomsubgmo  43205  fourierdlem42  46164  fourierdlem97  46218  clnbgrgrimlem  47901  line2  48673  itscnhlinecirc02plem2  48704