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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  soisores  7302  frrlem4  8268  omopth2  8548  ttrcltr  9669  fin23lem11  10270  dedekind  11337  xaddass  13209  swrdsbslen  14629  swrdspsleq  14630  ntrivcvgmul  15868  pockthg  16877  gsumsgrpccat  18767  efgred  19678  decpmatmullem  22658  decpmatmul  22659  unconn  23316  basqtop  23598  utop2nei  24138  ucncn  24172  cxple2  26606  cxple2a  26608  nogesgn1ores  27586  nolt02o  27607  nogt01o  27608  nosupbnd1lem1  27620  nosupbnd1lem3  27622  nosupbnd1lem4  27623  nosupbnd1lem5  27624  noinfbnd1lem1  27635  noinfbnd1lem3  27637  noinfbnd1lem4  27638  noinfbnd1lem5  27639  noetalem1  27653  cofcut1  27828  ax5seglem1  28855  ax5seglem2  28856  axpasch  28868  axcontlem4  28894  1pthon2v  30082  mhmimasplusg  32979  cvmlift2lem10  35299  br4  35745  cgrcomim  35977  btwnintr  36007  btwnouttr2  36010  btwndiff  36015  btwnconn1lem14  36088  btwnconn3  36091  segcon2  36093  brsegle  36096  brsegle2  36097  segleantisym  36103  seglelin  36104  outsideofeu  36119  eqlkr  39092  eqlkr2  39093  lkrlsp  39095  atbtwn  39440  athgt  39450  3dimlem3  39455  3dimlem3OLDN  39456  3dim3  39463  3atlem7  39483  4atlem0a  39587  4atlem3a  39591  4atlem11  39603  lneq2at  39772  lnatexN  39773  cdlemb  39788  paddasslem6  39819  llnexchb2  39863  lhp2lt  39995  lhpexle2lem  40003  lhpexle3  40006  lhpmcvr3  40019  lhpat3  40040  ltrnnidn  40168  ltrneq3  40202  cdleme17b  40281  cdleme25a  40347  cdleme25dN  40350  cdleme27cl  40360  cdlemefrs29bpre0  40390  cdlemefs32sn1aw  40408  cdleme32le  40441  cdleme46f2g2  40487  cdleme46f2g1  40488  cdleme50trn3  40547  trlord  40563  ltrniotavalbN  40578  cdlemg6  40617  cdlemg7N  40620  cdlemg11b  40636  cdlemg15a  40649  cdlemg15  40650  cdlemg39  40710  trlcone  40722  cdlemg42  40723  tendoconid  40823  tendotr  40824  cdlemk39u  40962  cdlemk19u  40964  cdleml5N  40974  cdlemm10N  41112  dihord11b  41216  dihord2pre  41219  dihvalcqpre  41229  dihopelvalcpre  41242  dihord6apre  41250  dihord4  41252  dihord5b  41253  dihglblem5apreN  41285  dihmeetlem13N  41313  dihmeetlem19N  41319  dih1dimatlem0  41322  qirropth  42896  mzpcong  42961  jm2.25lem1  42987  jm2.26  42991  idomsubgmo  43182  fourierdlem42  46147  fourierdlem97  46201  clnbgrgrimlem  47933  line2  48741  itscnhlinecirc02plem2  48772