Theorem simpl2l 1222

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  soisores  7083  omopth2  8213  fin23lem11  9742  dedekind  10806  xaddass  12645  swrdsbslen  14029  swrdspsleq  14030  ntrivcvgmul  15261  pockthg  16245  gsumsgrpccat  18007  efgred  18877  decpmatmullem  21382  decpmatmul  21383  unconn  22040  basqtop  22322  utop2nei  22862  ucncn  22897  cxple2  25283  cxple2a  25285  ax5seglem1  26717  ax5seglem2  26718  axpasch  26730  axcontlem4  26756  1pthon2v  27935  cvmlift2lem10  32563  br4  32998  frrlem4  33130  nolt02o  33203  nosupbnd1lem1  33212  nosupbnd1lem3  33214  nosupbnd1lem4  33215  nosupbnd1lem5  33216  cgrcomim  33454  btwnintr  33484  btwnouttr2  33487  btwndiff  33492  btwnconn1lem14  33565  btwnconn3  33568  segcon2  33570  brsegle  33573  brsegle2  33574  segleantisym  33580  seglelin  33581  outsideofeu  33596  eqlkr  36239  eqlkr2  36240  lkrlsp  36242  atbtwn  36586  athgt  36596  3dimlem3  36601  3dimlem3OLDN  36602  3dim3  36609  3atlem7  36629  4atlem0a  36733  4atlem3a  36737  4atlem11  36749  lneq2at  36918  lnatexN  36919  cdlemb  36934  paddasslem6  36965  llnexchb2  37009  lhp2lt  37141  lhpexle2lem  37149  lhpexle3  37152  lhpmcvr3  37165  lhpat3  37186  ltrnnidn  37314  ltrneq3  37348  cdleme17b  37427  cdleme25a  37493  cdleme25dN  37496  cdleme27cl  37506  cdlemefrs29bpre0  37536  cdlemefs32sn1aw  37554  cdleme32le  37587  cdleme46f2g2  37633  cdleme46f2g1  37634  cdleme50trn3  37693  trlord  37709  ltrniotavalbN  37724  cdlemg6  37763  cdlemg7N  37766  cdlemg11b  37782  cdlemg15a  37795  cdlemg15  37796  cdlemg39  37856  trlcone  37868  cdlemg42  37869  tendoconid  37969  tendotr  37970  cdlemk39u  38108  cdlemk19u  38110  cdleml5N  38120  cdlemm10N  38258  dihord11b  38362  dihord2pre  38365  dihvalcqpre  38375  dihopelvalcpre  38388  dihord6apre  38396  dihord4  38398  dihord5b  38399  dihglblem5apreN  38431  dihmeetlem13N  38459  dihmeetlem19N  38465  dih1dimatlem0  38468  qirropth  39511  mzpcong  39575  jm2.25lem1  39601  jm2.26  39605  idomsubgmo  39804  fourierdlem42  42441  fourierdlem97  42495  line2  44746  itscnhlinecirc02plem2  44777