Theorem simpl2l 1227

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 766	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜑)
2	1	3ad2antl2 1187	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  7268  frrlem4  8229  omopth2  8509  ttrcltr  9631  fin23lem11  10230  dedekind  11297  xaddass  13169  swrdsbslen  14589  swrdspsleq  14590  ntrivcvgmul  15827  pockthg  16836  gsumsgrpccat  18732  efgred  19645  decpmatmullem  22674  decpmatmul  22675  unconn  23332  basqtop  23614  utop2nei  24154  ucncn  24188  cxple2  26622  cxple2a  26624  nogesgn1ores  27602  nolt02o  27623  nogt01o  27624  nosupbnd1lem1  27636  nosupbnd1lem3  27638  nosupbnd1lem4  27639  nosupbnd1lem5  27640  noinfbnd1lem1  27651  noinfbnd1lem3  27653  noinfbnd1lem4  27654  noinfbnd1lem5  27655  noetalem1  27669  cofcut1  27851  ax5seglem1  28891  ax5seglem2  28892  axpasch  28904  axcontlem4  28930  1pthon2v  30115  mhmimasplusg  33005  cvmlift2lem10  35284  br4  35730  cgrcomim  35962  btwnintr  35992  btwnouttr2  35995  btwndiff  36000  btwnconn1lem14  36073  btwnconn3  36076  segcon2  36078  brsegle  36081  brsegle2  36082  segleantisym  36088  seglelin  36089  outsideofeu  36104  eqlkr  39077  eqlkr2  39078  lkrlsp  39080  atbtwn  39425  athgt  39435  3dimlem3  39440  3dimlem3OLDN  39441  3dim3  39448  3atlem7  39468  4atlem0a  39572  4atlem3a  39576  4atlem11  39588  lneq2at  39757  lnatexN  39758  cdlemb  39773  paddasslem6  39804  llnexchb2  39848  lhp2lt  39980  lhpexle2lem  39988  lhpexle3  39991  lhpmcvr3  40004  lhpat3  40025  ltrnnidn  40153  ltrneq3  40187  cdleme17b  40266  cdleme25a  40332  cdleme25dN  40335  cdleme27cl  40345  cdlemefrs29bpre0  40375  cdlemefs32sn1aw  40393  cdleme32le  40426  cdleme46f2g2  40472  cdleme46f2g1  40473  cdleme50trn3  40532  trlord  40548  ltrniotavalbN  40563  cdlemg6  40602  cdlemg7N  40605  cdlemg11b  40621  cdlemg15a  40634  cdlemg15  40635  cdlemg39  40695  trlcone  40707  cdlemg42  40708  tendoconid  40808  tendotr  40809  cdlemk39u  40947  cdlemk19u  40949  cdleml5N  40959  cdlemm10N  41097  dihord11b  41201  dihord2pre  41204  dihvalcqpre  41214  dihopelvalcpre  41227  dihord6apre  41235  dihord4  41237  dihord5b  41238  dihglblem5apreN  41270  dihmeetlem13N  41298  dihmeetlem19N  41304  dih1dimatlem0  41307  qirropth  42881  mzpcong  42945  jm2.25lem1  42971  jm2.26  42975  idomsubgmo  43166  fourierdlem42  46131  fourierdlem97  46185  clnbgrgrimlem  47918  line2  48738  itscnhlinecirc02plem2  48769