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  7336  frrlem4  8295  omopth2  8578  ttrcltr  9695  fin23lem11  10319  dedekind  11391  xaddass  13293  swrdsbslen  14726  swrdspsleq  14727  ntrivcvgmul  15982  pockthg  16991  gsumsgrpccat  18930  efgred  19849  decpmatmullem  22965  decpmatmul  22966  unconn  23623  basqtop  23905  utop2nei  24444  ucncn  24478  cxple2  26899  cxple2a  26901  nogesgn1ores  27875  nolt02o  27896  nogt01o  27897  nosupbnd1lem1  27909  nosupbnd1lem3  27911  nosupbnd1lem4  27912  nosupbnd1lem5  27913  noinfbnd1lem1  27924  noinfbnd1lem3  27926  noinfbnd1lem4  27927  noinfbnd1lem5  27928  noetalem1  27942  cofcut1  28150  bdayfinbndlem1  28697  ax5seglem1  29315  ax5seglem2  29316  axpasch  29328  axcontlem4  29354  1pthon2v  30541  mhmimasplusg  33388  cvmlift2lem10  35825  br4  36271  cgrcomim  36502  btwnintr  36532  btwnouttr2  36535  btwndiff  36540  btwnconn1lem14  36613  btwnconn3  36616  segcon2  36618  brsegle  36621  brsegle2  36622  segleantisym  36628  seglelin  36629  outsideofeu  36644  eqlkr  39914  eqlkr2  39915  lkrlsp  39917  atbtwn  40261  athgt  40271  3dimlem3  40276  3dimlem3OLDN  40277  3dim3  40284  3atlem7  40304  4atlem0a  40408  4atlem3a  40412  4atlem11  40424  lneq2at  40593  lnatexN  40594  cdlemb  40609  paddasslem6  40640  llnexchb2  40684  lhp2lt  40816  lhpexle2lem  40824  lhpexle3  40827  lhpmcvr3  40840  lhpat3  40861  ltrnnidn  40989  ltrneq3  41023  cdleme17b  41102  cdleme25a  41168  cdleme25dN  41171  cdleme27cl  41181  cdlemefrs29bpre0  41211  cdlemefs32sn1aw  41229  cdleme32le  41262  cdleme46f2g2  41308  cdleme46f2g1  41309  cdleme50trn3  41368  trlord  41384  ltrniotavalbN  41399  cdlemg6  41438  cdlemg7N  41441  cdlemg11b  41457  cdlemg15a  41470  cdlemg15  41471  cdlemg39  41531  trlcone  41543  cdlemg42  41544  tendoconid  41644  tendotr  41645  cdlemk39u  41783  cdlemk19u  41785  cdleml5N  41795  cdlemm10N  41933  dihord11b  42037  dihord2pre  42040  dihvalcqpre  42050  dihopelvalcpre  42063  dihord6apre  42071  dihord4  42073  dihord5b  42074  dihglblem5apreN  42106  dihmeetlem13N  42134  dihmeetlem19N  42140  dih1dimatlem0  42143  qirropth  43676  mzpcong  43740  jm2.25lem1  43766  jm2.26  43770  idomsubgmo  43961  fourierdlem42  46904  fourierdlem97  46958  clnbgrgrimlem  48739  line2  49573  itscnhlinecirc02plem2  49604