Theorem simpl2l 1233

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  soisores  7278  frrlem4  8236  omopth2  8516  ttrcltr  9635  fin23lem11  10237  dedekind  11307  xaddass  13199  swrdsbslen  14625  swrdspsleq  14626  ntrivcvgmul  15865  pockthg  16875  gsumsgrpccat  18806  efgred  19721  decpmatmullem  22761  decpmatmul  22762  unconn  23419  basqtop  23701  utop2nei  24240  ucncn  24274  cxple2  26686  cxple2a  26688  nogesgn1ores  27663  nolt02o  27684  nogt01o  27685  nosupbnd1lem1  27697  nosupbnd1lem3  27699  nosupbnd1lem4  27700  nosupbnd1lem5  27701  noinfbnd1lem1  27712  noinfbnd1lem3  27714  noinfbnd1lem4  27715  noinfbnd1lem5  27716  noetalem1  27730  cofcut1  27937  bdayfinbndlem1  28484  ax5seglem1  29022  ax5seglem2  29023  axpasch  29035  axcontlem4  29061  1pthon2v  30248  mhmimasplusg  33124  cvmlift2lem10  35547  br4  35993  cgrcomim  36224  btwnintr  36254  btwnouttr2  36257  btwndiff  36262  btwnconn1lem14  36335  btwnconn3  36338  segcon2  36340  brsegle  36343  brsegle2  36344  segleantisym  36350  seglelin  36351  outsideofeu  36366  eqlkr  39598  eqlkr2  39599  lkrlsp  39601  atbtwn  39945  athgt  39955  3dimlem3  39960  3dimlem3OLDN  39961  3dim3  39968  3atlem7  39988  4atlem0a  40092  4atlem3a  40096  4atlem11  40108  lneq2at  40277  lnatexN  40278  cdlemb  40293  paddasslem6  40324  llnexchb2  40368  lhp2lt  40500  lhpexle2lem  40508  lhpexle3  40511  lhpmcvr3  40524  lhpat3  40545  ltrnnidn  40673  ltrneq3  40707  cdleme17b  40786  cdleme25a  40852  cdleme25dN  40855  cdleme27cl  40865  cdlemefrs29bpre0  40895  cdlemefs32sn1aw  40913  cdleme32le  40946  cdleme46f2g2  40992  cdleme46f2g1  40993  cdleme50trn3  41052  trlord  41068  ltrniotavalbN  41083  cdlemg6  41122  cdlemg7N  41125  cdlemg11b  41141  cdlemg15a  41154  cdlemg15  41155  cdlemg39  41215  trlcone  41227  cdlemg42  41228  tendoconid  41328  tendotr  41329  cdlemk39u  41467  cdlemk19u  41469  cdleml5N  41479  cdlemm10N  41617  dihord11b  41721  dihord2pre  41724  dihvalcqpre  41734  dihopelvalcpre  41747  dihord6apre  41755  dihord4  41757  dihord5b  41758  dihglblem5apreN  41790  dihmeetlem13N  41818  dihmeetlem19N  41824  dih1dimatlem0  41827  qirropth  43360  mzpcong  43424  jm2.25lem1  43450  jm2.26  43454  idomsubgmo  43645  fourierdlem42  46599  fourierdlem97  46653  clnbgrgrimlem  48431  line2  49250  itscnhlinecirc02plem2  49281