Theorem simpl2l 1226

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

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

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 1089

This theorem is referenced by:  soisores  7323  frrlem4  8273  omopth2  8583  ttrcltr  9710  fin23lem11  10311  dedekind  11376  xaddass  13227  swrdsbslen  14613  swrdspsleq  14614  ntrivcvgmul  15847  pockthg  16838  gsumsgrpccat  18720  efgred  19615  decpmatmullem  22272  decpmatmul  22273  unconn  22932  basqtop  23214  utop2nei  23754  ucncn  23789  cxple2  26204  cxple2a  26206  nogesgn1ores  27174  nolt02o  27195  nogt01o  27196  nosupbnd1lem1  27208  nosupbnd1lem3  27210  nosupbnd1lem4  27211  nosupbnd1lem5  27212  noinfbnd1lem1  27223  noinfbnd1lem3  27225  noinfbnd1lem4  27226  noinfbnd1lem5  27227  noetalem1  27241  cofcut1  27404  ax5seglem1  28183  ax5seglem2  28184  axpasch  28196  axcontlem4  28222  1pthon2v  29403  cvmlift2lem10  34298  br4  34723  cgrcomim  34956  btwnintr  34986  btwnouttr2  34989  btwndiff  34994  btwnconn1lem14  35067  btwnconn3  35070  segcon2  35072  brsegle  35075  brsegle2  35076  segleantisym  35082  seglelin  35083  outsideofeu  35098  eqlkr  37964  eqlkr2  37965  lkrlsp  37967  atbtwn  38312  athgt  38322  3dimlem3  38327  3dimlem3OLDN  38328  3dim3  38335  3atlem7  38355  4atlem0a  38459  4atlem3a  38463  4atlem11  38475  lneq2at  38644  lnatexN  38645  cdlemb  38660  paddasslem6  38691  llnexchb2  38735  lhp2lt  38867  lhpexle2lem  38875  lhpexle3  38878  lhpmcvr3  38891  lhpat3  38912  ltrnnidn  39040  ltrneq3  39074  cdleme17b  39153  cdleme25a  39219  cdleme25dN  39222  cdleme27cl  39232  cdlemefrs29bpre0  39262  cdlemefs32sn1aw  39280  cdleme32le  39313  cdleme46f2g2  39359  cdleme46f2g1  39360  cdleme50trn3  39419  trlord  39435  ltrniotavalbN  39450  cdlemg6  39489  cdlemg7N  39492  cdlemg11b  39508  cdlemg15a  39521  cdlemg15  39522  cdlemg39  39582  trlcone  39594  cdlemg42  39595  tendoconid  39695  tendotr  39696  cdlemk39u  39834  cdlemk19u  39836  cdleml5N  39846  cdlemm10N  39984  dihord11b  40088  dihord2pre  40091  dihvalcqpre  40101  dihopelvalcpre  40114  dihord6apre  40122  dihord4  40124  dihord5b  40125  dihglblem5apreN  40157  dihmeetlem13N  40185  dihmeetlem19N  40191  dih1dimatlem0  40194  qirropth  41636  mzpcong  41701  jm2.25lem1  41727  jm2.26  41731  idomsubgmo  41930  fourierdlem42  44855  fourierdlem97  44909  line2  47428  itscnhlinecirc02plem2  47459