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  7335  frrlem4  8310  omopth2  8595  ttrcltr  9720  fin23lem11  10398  dedekind  11476  xaddass  13382  swrdsbslen  14818  swrdspsleq  14819  ntrivcvgmul  16076  pockthg  17089  gsumsgrpccat  19041  efgred  19967  decpmatmullem  23094  decpmatmul  23095  unconn  23752  basqtop  24035  utop2nei  24574  ucncn  24608  cxple2  27030  cxple2a  27032  nogesgn1ores  28036  nolt02o  28057  nogt01o  28058  nosupbnd1lem1  28070  nosupbnd1lem3  28072  nosupbnd1lem4  28073  nosupbnd1lem5  28074  noinfbnd1lem1  28085  noinfbnd1lem3  28087  noinfbnd1lem4  28088  noinfbnd1lem5  28089  noetalem1  28103  cofcut1  28311  bdayfinbndlem1  28858  ax5seglem1  29511  ax5seglem2  29512  axpasch  29524  axcontlem4  29550  1pthon2v  30759  mhmimasplusg  33644  cvmlift2lem10  36163  br4  36615  cgrcomim  36846  btwnintr  36876  btwnouttr2  36879  btwndiff  36884  btwnconn1lem14  36957  btwnconn3  36960  segcon2  36962  brsegle  36965  brsegle2  36966  segleantisym  36972  seglelin  36973  outsideofeu  36988  eqlkr  40249  eqlkr2  40250  lkrlsp  40252  atbtwn  40596  athgt  40606  3dimlem3  40611  3dimlem3OLDN  40612  3dim3  40619  3atlem7  40639  4atlem0a  40743  4atlem3a  40747  4atlem11  40759  lneq2at  40928  lnatexN  40929  cdlemb  40944  paddasslem6  40975  llnexchb2  41019  lhp2lt  41151  lhpexle2lem  41159  lhpexle3  41162  lhpmcvr3  41175  lhpat3  41196  ltrnnidn  41324  ltrneq3  41358  cdleme17b  41437  cdleme25a  41503  cdleme25dN  41506  cdleme27cl  41516  cdlemefrs29bpre0  41546  cdlemefs32sn1aw  41564  cdleme32le  41597  cdleme46f2g2  41643  cdleme46f2g1  41644  cdleme50trn3  41703  trlord  41719  ltrniotavalbN  41734  cdlemg6  41773  cdlemg7N  41776  cdlemg11b  41792  cdlemg15a  41805  cdlemg15  41806  cdlemg39  41866  trlcone  41878  cdlemg42  41879  tendoconid  41979  tendotr  41980  cdlemk39u  42118  cdlemk19u  42120  cdleml5N  42130  cdlemm10N  42268  dihord11b  42372  dihord2pre  42375  dihvalcqpre  42385  dihopelvalcpre  42398  dihord6apre  42406  dihord4  42408  dihord5b  42409  dihglblem5apreN  42441  dihmeetlem13N  42469  dihmeetlem19N  42475  dih1dimatlem0  42478  qirropth  44008  mzpcong  44072  jm2.25lem1  44098  jm2.26  44102  idomsubgmo  44288  fourierdlem42  47252  fourierdlem97  47306  clnbgrgrimlem  49124  line2  49957  itscnhlinecirc02plem2  49988