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  7248  frrlem4  8167  omopth2  8478  ttrcltr  9565  fin23lem11  10166  dedekind  11231  xaddass  13076  swrdsbslen  14467  swrdspsleq  14468  ntrivcvgmul  15705  pockthg  16696  gsumsgrpccat  18567  efgred  19441  decpmatmullem  22018  decpmatmul  22019  unconn  22678  basqtop  22960  utop2nei  23500  ucncn  23535  cxple2  25950  cxple2a  25952  nogesgn1ores  26920  nolt02o  26941  nogt01o  26942  nosupbnd1lem1  26954  nosupbnd1lem3  26956  nosupbnd1lem4  26957  nosupbnd1lem5  26958  noinfbnd1lem1  26969  noinfbnd1lem3  26971  noinfbnd1lem4  26972  noinfbnd1lem5  26973  noetalem1  26987  ax5seglem1  27526  ax5seglem2  27527  axpasch  27539  axcontlem4  27565  1pthon2v  28746  cvmlift2lem10  33514  br4  33958  cofcut1  34181  cgrcomim  34382  btwnintr  34412  btwnouttr2  34415  btwndiff  34420  btwnconn1lem14  34493  btwnconn3  34496  segcon2  34498  brsegle  34501  brsegle2  34502  segleantisym  34508  seglelin  34509  outsideofeu  34524  eqlkr  37359  eqlkr2  37360  lkrlsp  37362  atbtwn  37707  athgt  37717  3dimlem3  37722  3dimlem3OLDN  37723  3dim3  37730  3atlem7  37750  4atlem0a  37854  4atlem3a  37858  4atlem11  37870  lneq2at  38039  lnatexN  38040  cdlemb  38055  paddasslem6  38086  llnexchb2  38130  lhp2lt  38262  lhpexle2lem  38270  lhpexle3  38273  lhpmcvr3  38286  lhpat3  38307  ltrnnidn  38435  ltrneq3  38469  cdleme17b  38548  cdleme25a  38614  cdleme25dN  38617  cdleme27cl  38627  cdlemefrs29bpre0  38657  cdlemefs32sn1aw  38675  cdleme32le  38708  cdleme46f2g2  38754  cdleme46f2g1  38755  cdleme50trn3  38814  trlord  38830  ltrniotavalbN  38845  cdlemg6  38884  cdlemg7N  38887  cdlemg11b  38903  cdlemg15a  38916  cdlemg15  38917  cdlemg39  38977  trlcone  38989  cdlemg42  38990  tendoconid  39090  tendotr  39091  cdlemk39u  39229  cdlemk19u  39231  cdleml5N  39241  cdlemm10N  39379  dihord11b  39483  dihord2pre  39486  dihvalcqpre  39496  dihopelvalcpre  39509  dihord6apre  39517  dihord4  39519  dihord5b  39520  dihglblem5apreN  39552  dihmeetlem13N  39580  dihmeetlem19N  39586  dih1dimatlem0  39589  qirropth  40980  mzpcong  41045  jm2.25lem1  41071  jm2.26  41075  idomsubgmo  41274  fourierdlem42  44015  fourierdlem97  44069  line2  46438  itscnhlinecirc02plem2  46469