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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  soisores  7346  frrlem4  8312  omopth2  8620  ttrcltr  9753  fin23lem11  10354  dedekind  11421  xaddass  13287  swrdsbslen  14698  swrdspsleq  14699  ntrivcvgmul  15934  pockthg  16939  gsumsgrpccat  18865  efgred  19780  decpmatmullem  22792  decpmatmul  22793  unconn  23452  basqtop  23734  utop2nei  24274  ucncn  24309  cxple2  26753  cxple2a  26755  nogesgn1ores  27733  nolt02o  27754  nogt01o  27755  nosupbnd1lem1  27767  nosupbnd1lem3  27769  nosupbnd1lem4  27770  nosupbnd1lem5  27771  noinfbnd1lem1  27782  noinfbnd1lem3  27784  noinfbnd1lem4  27785  noinfbnd1lem5  27786  noetalem1  27800  cofcut1  27968  ax5seglem1  28957  ax5seglem2  28958  axpasch  28970  axcontlem4  28996  1pthon2v  30181  mhmimasplusg  33025  cvmlift2lem10  35296  br4  35737  cgrcomim  35970  btwnintr  36000  btwnouttr2  36003  btwndiff  36008  btwnconn1lem14  36081  btwnconn3  36084  segcon2  36086  brsegle  36089  brsegle2  36090  segleantisym  36096  seglelin  36097  outsideofeu  36112  eqlkr  39080  eqlkr2  39081  lkrlsp  39083  atbtwn  39428  athgt  39438  3dimlem3  39443  3dimlem3OLDN  39444  3dim3  39451  3atlem7  39471  4atlem0a  39575  4atlem3a  39579  4atlem11  39591  lneq2at  39760  lnatexN  39761  cdlemb  39776  paddasslem6  39807  llnexchb2  39851  lhp2lt  39983  lhpexle2lem  39991  lhpexle3  39994  lhpmcvr3  40007  lhpat3  40028  ltrnnidn  40156  ltrneq3  40190  cdleme17b  40269  cdleme25a  40335  cdleme25dN  40338  cdleme27cl  40348  cdlemefrs29bpre0  40378  cdlemefs32sn1aw  40396  cdleme32le  40429  cdleme46f2g2  40475  cdleme46f2g1  40476  cdleme50trn3  40535  trlord  40551  ltrniotavalbN  40566  cdlemg6  40605  cdlemg7N  40608  cdlemg11b  40624  cdlemg15a  40637  cdlemg15  40638  cdlemg39  40698  trlcone  40710  cdlemg42  40711  tendoconid  40811  tendotr  40812  cdlemk39u  40950  cdlemk19u  40952  cdleml5N  40962  cdlemm10N  41100  dihord11b  41204  dihord2pre  41207  dihvalcqpre  41217  dihopelvalcpre  41230  dihord6apre  41238  dihord4  41240  dihord5b  41241  dihglblem5apreN  41273  dihmeetlem13N  41301  dihmeetlem19N  41307  dih1dimatlem0  41310  qirropth  42895  mzpcong  42960  jm2.25lem1  42986  jm2.26  42990  idomsubgmo  43181  fourierdlem42  46104  fourierdlem97  46158  clnbgrgrimlem  47838  line2  48601  itscnhlinecirc02plem2  48632