Theorem simpl2l 1245

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  soisores  7327  frrlem4  8291  omopth2  8576  ttrcltr  9701  fin23lem11  10376  dedekind  11454  xaddass  13360  swrdsbslen  14794  swrdspsleq  14795  ntrivcvgmul  16051  pockthg  17064  gsumsgrpccat  19016  efgred  19942  decpmatmullem  23069  decpmatmul  23070  unconn  23727  basqtop  24010  utop2nei  24549  ucncn  24583  cxple2  27007  cxple2a  27009  nogesgn1ores  28013  nolt02o  28034  nogt01o  28035  nosupbnd1lem1  28047  nosupbnd1lem3  28049  nosupbnd1lem4  28050  nosupbnd1lem5  28051  noinfbnd1lem1  28062  noinfbnd1lem3  28064  noinfbnd1lem4  28065  noinfbnd1lem5  28066  noetalem1  28080  cofcut1  28288  bdayfinbndlem1  28835  ax5seglem1  29488  ax5seglem2  29489  axpasch  29501  axcontlem4  29527  1pthon2v  30736  mhmimasplusg  33580  cvmlift2lem10  36046  br4  36492  cgrcomim  36724  btwnintr  36754  btwnouttr2  36757  btwndiff  36762  btwnconn1lem14  36835  btwnconn3  36838  segcon2  36840  brsegle  36843  brsegle2  36844  segleantisym  36850  seglelin  36851  outsideofeu  36866  eqlkr  40124  eqlkr2  40125  lkrlsp  40127  atbtwn  40471  athgt  40481  3dimlem3  40486  3dimlem3OLDN  40487  3dim3  40494  3atlem7  40514  4atlem0a  40618  4atlem3a  40622  4atlem11  40634  lneq2at  40803  lnatexN  40804  cdlemb  40819  paddasslem6  40850  llnexchb2  40894  lhp2lt  41026  lhpexle2lem  41034  lhpexle3  41037  lhpmcvr3  41050  lhpat3  41071  ltrnnidn  41199  ltrneq3  41233  cdleme17b  41312  cdleme25a  41378  cdleme25dN  41381  cdleme27cl  41391  cdlemefrs29bpre0  41421  cdlemefs32sn1aw  41439  cdleme32le  41472  cdleme46f2g2  41518  cdleme46f2g1  41519  cdleme50trn3  41578  trlord  41594  ltrniotavalbN  41609  cdlemg6  41648  cdlemg7N  41651  cdlemg11b  41667  cdlemg15a  41680  cdlemg15  41681  cdlemg39  41741  trlcone  41753  cdlemg42  41754  tendoconid  41854  tendotr  41855  cdlemk39u  41993  cdlemk19u  41995  cdleml5N  42005  cdlemm10N  42143  dihord11b  42247  dihord2pre  42250  dihvalcqpre  42260  dihopelvalcpre  42273  dihord6apre  42281  dihord4  42283  dihord5b  42284  dihglblem5apreN  42316  dihmeetlem13N  42344  dihmeetlem19N  42350  dih1dimatlem0  42353  qirropth  43868  mzpcong  43932  jm2.25lem1  43958  jm2.26  43962  idomsubgmo  44153  fourierdlem42  47103  fourierdlem97  47157  clnbgrgrimlem  48975  line2  49808  itscnhlinecirc02plem2  49839