Theorem simpl2l 1225

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

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

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  soisores  7207  frrlem4  8114  omopth2  8424  ttrcltr  9483  fin23lem11  10082  dedekind  11147  xaddass  12992  swrdsbslen  14386  swrdspsleq  14387  ntrivcvgmul  15623  pockthg  16616  gsumsgrpccat  18487  efgred  19363  decpmatmullem  21929  decpmatmul  21930  unconn  22589  basqtop  22871  utop2nei  23411  ucncn  23446  cxple2  25861  cxple2a  25863  ax5seglem1  27305  ax5seglem2  27306  axpasch  27318  axcontlem4  27344  1pthon2v  28526  cvmlift2lem10  33283  br4  33734  nogesgn1ores  33886  nolt02o  33907  nogt01o  33908  nosupbnd1lem1  33920  nosupbnd1lem3  33922  nosupbnd1lem4  33923  nosupbnd1lem5  33924  noinfbnd1lem1  33935  noinfbnd1lem3  33937  noinfbnd1lem4  33938  noinfbnd1lem5  33939  noetalem1  33953  cofcut1  34099  cgrcomim  34300  btwnintr  34330  btwnouttr2  34333  btwndiff  34338  btwnconn1lem14  34411  btwnconn3  34414  segcon2  34416  brsegle  34419  brsegle2  34420  segleantisym  34426  seglelin  34427  outsideofeu  34442  eqlkr  37120  eqlkr2  37121  lkrlsp  37123  atbtwn  37467  athgt  37477  3dimlem3  37482  3dimlem3OLDN  37483  3dim3  37490  3atlem7  37510  4atlem0a  37614  4atlem3a  37618  4atlem11  37630  lneq2at  37799  lnatexN  37800  cdlemb  37815  paddasslem6  37846  llnexchb2  37890  lhp2lt  38022  lhpexle2lem  38030  lhpexle3  38033  lhpmcvr3  38046  lhpat3  38067  ltrnnidn  38195  ltrneq3  38229  cdleme17b  38308  cdleme25a  38374  cdleme25dN  38377  cdleme27cl  38387  cdlemefrs29bpre0  38417  cdlemefs32sn1aw  38435  cdleme32le  38468  cdleme46f2g2  38514  cdleme46f2g1  38515  cdleme50trn3  38574  trlord  38590  ltrniotavalbN  38605  cdlemg6  38644  cdlemg7N  38647  cdlemg11b  38663  cdlemg15a  38676  cdlemg15  38677  cdlemg39  38737  trlcone  38749  cdlemg42  38750  tendoconid  38850  tendotr  38851  cdlemk39u  38989  cdlemk19u  38991  cdleml5N  39001  cdlemm10N  39139  dihord11b  39243  dihord2pre  39246  dihvalcqpre  39256  dihopelvalcpre  39269  dihord6apre  39277  dihord4  39279  dihord5b  39280  dihglblem5apreN  39312  dihmeetlem13N  39340  dihmeetlem19N  39346  dih1dimatlem0  39349  qirropth  40737  mzpcong  40801  jm2.25lem1  40827  jm2.26  40831  idomsubgmo  41030  fourierdlem42  43697  fourierdlem97  43751  line2  46109  itscnhlinecirc02plem2  46140