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  7332  frrlem4  8292  omopth2  8575  ttrcltr  9699  fin23lem11  10323  dedekind  11401  xaddass  13305  swrdsbslen  14738  swrdspsleq  14739  ntrivcvgmul  15995  pockthg  17004  gsumsgrpccat  18955  efgred  19881  decpmatmullem  23002  decpmatmul  23003  unconn  23660  basqtop  23943  utop2nei  24482  ucncn  24516  cxple2  26942  cxple2a  26944  nogesgn1ores  27918  nolt02o  27939  nogt01o  27940  nosupbnd1lem1  27952  nosupbnd1lem3  27954  nosupbnd1lem4  27955  nosupbnd1lem5  27956  noinfbnd1lem1  27967  noinfbnd1lem3  27969  noinfbnd1lem4  27970  noinfbnd1lem5  27971  noetalem1  27985  cofcut1  28193  bdayfinbndlem1  28740  ax5seglem1  29393  ax5seglem2  29394  axpasch  29406  axcontlem4  29432  1pthon2v  30641  mhmimasplusg  33485  cvmlift2lem10  35899  br4  36345  cgrcomim  36577  btwnintr  36607  btwnouttr2  36610  btwndiff  36615  btwnconn1lem14  36688  btwnconn3  36691  segcon2  36693  brsegle  36696  brsegle2  36697  segleantisym  36703  seglelin  36704  outsideofeu  36719  eqlkr  39980  eqlkr2  39981  lkrlsp  39983  atbtwn  40327  athgt  40337  3dimlem3  40342  3dimlem3OLDN  40343  3dim3  40350  3atlem7  40370  4atlem0a  40474  4atlem3a  40478  4atlem11  40490  lneq2at  40659  lnatexN  40660  cdlemb  40675  paddasslem6  40706  llnexchb2  40750  lhp2lt  40882  lhpexle2lem  40890  lhpexle3  40893  lhpmcvr3  40906  lhpat3  40927  ltrnnidn  41055  ltrneq3  41089  cdleme17b  41168  cdleme25a  41234  cdleme25dN  41237  cdleme27cl  41247  cdlemefrs29bpre0  41277  cdlemefs32sn1aw  41295  cdleme32le  41328  cdleme46f2g2  41374  cdleme46f2g1  41375  cdleme50trn3  41434  trlord  41450  ltrniotavalbN  41465  cdlemg6  41504  cdlemg7N  41507  cdlemg11b  41523  cdlemg15a  41536  cdlemg15  41537  cdlemg39  41597  trlcone  41609  cdlemg42  41610  tendoconid  41710  tendotr  41711  cdlemk39u  41849  cdlemk19u  41851  cdleml5N  41861  cdlemm10N  41999  dihord11b  42103  dihord2pre  42106  dihvalcqpre  42116  dihopelvalcpre  42129  dihord6apre  42137  dihord4  42139  dihord5b  42140  dihglblem5apreN  42172  dihmeetlem13N  42200  dihmeetlem19N  42206  dih1dimatlem0  42209  qirropth  43757  mzpcong  43821  jm2.25lem1  43847  jm2.26  43851  idomsubgmo  44042  fourierdlem42  46985  fourierdlem97  47039  clnbgrgrimlem  48857  line2  49690  itscnhlinecirc02plem2  49721