Theorem simpl2l 1224

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

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  soisores  7178  frrlem4  8076  omopth2  8377  fin23lem11  10004  dedekind  11068  xaddass  12912  swrdsbslen  14305  swrdspsleq  14306  ntrivcvgmul  15542  pockthg  16535  gsumsgrpccat  18393  efgred  19269  decpmatmullem  21828  decpmatmul  21829  unconn  22488  basqtop  22770  utop2nei  23310  ucncn  23345  cxple2  25757  cxple2a  25759  ax5seglem1  27199  ax5seglem2  27200  axpasch  27212  axcontlem4  27238  1pthon2v  28418  cvmlift2lem10  33174  br4  33631  ttrcltr  33702  nogesgn1ores  33804  nolt02o  33825  nogt01o  33826  nosupbnd1lem1  33838  nosupbnd1lem3  33840  nosupbnd1lem4  33841  nosupbnd1lem5  33842  noinfbnd1lem1  33853  noinfbnd1lem3  33855  noinfbnd1lem4  33856  noinfbnd1lem5  33857  noetalem1  33871  cofcut1  34017  cgrcomim  34218  btwnintr  34248  btwnouttr2  34251  btwndiff  34256  btwnconn1lem14  34329  btwnconn3  34332  segcon2  34334  brsegle  34337  brsegle2  34338  segleantisym  34344  seglelin  34345  outsideofeu  34360  eqlkr  37040  eqlkr2  37041  lkrlsp  37043  atbtwn  37387  athgt  37397  3dimlem3  37402  3dimlem3OLDN  37403  3dim3  37410  3atlem7  37430  4atlem0a  37534  4atlem3a  37538  4atlem11  37550  lneq2at  37719  lnatexN  37720  cdlemb  37735  paddasslem6  37766  llnexchb2  37810  lhp2lt  37942  lhpexle2lem  37950  lhpexle3  37953  lhpmcvr3  37966  lhpat3  37987  ltrnnidn  38115  ltrneq3  38149  cdleme17b  38228  cdleme25a  38294  cdleme25dN  38297  cdleme27cl  38307  cdlemefrs29bpre0  38337  cdlemefs32sn1aw  38355  cdleme32le  38388  cdleme46f2g2  38434  cdleme46f2g1  38435  cdleme50trn3  38494  trlord  38510  ltrniotavalbN  38525  cdlemg6  38564  cdlemg7N  38567  cdlemg11b  38583  cdlemg15a  38596  cdlemg15  38597  cdlemg39  38657  trlcone  38669  cdlemg42  38670  tendoconid  38770  tendotr  38771  cdlemk39u  38909  cdlemk19u  38911  cdleml5N  38921  cdlemm10N  39059  dihord11b  39163  dihord2pre  39166  dihvalcqpre  39176  dihopelvalcpre  39189  dihord6apre  39197  dihord4  39199  dihord5b  39200  dihglblem5apreN  39232  dihmeetlem13N  39260  dihmeetlem19N  39266  dih1dimatlem0  39269  qirropth  40646  mzpcong  40710  jm2.25lem1  40736  jm2.26  40740  idomsubgmo  40939  fourierdlem42  43580  fourierdlem97  43634  line2  45986  itscnhlinecirc02plem2  46017