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  7267  frrlem4  8225  omopth2  8505  ttrcltr  9613  fin23lem11  10215  dedekind  11283  xaddass  13150  swrdsbslen  14574  swrdspsleq  14575  ntrivcvgmul  15811  pockthg  16820  gsumsgrpccat  18750  efgred  19662  decpmatmullem  22687  decpmatmul  22688  unconn  23345  basqtop  23627  utop2nei  24166  ucncn  24200  cxple2  26634  cxple2a  26636  nogesgn1ores  27614  nolt02o  27635  nogt01o  27636  nosupbnd1lem1  27648  nosupbnd1lem3  27650  nosupbnd1lem4  27651  nosupbnd1lem5  27652  noinfbnd1lem1  27663  noinfbnd1lem3  27665  noinfbnd1lem4  27666  noinfbnd1lem5  27667  noetalem1  27681  cofcut1  27865  ax5seglem1  28908  ax5seglem2  28909  axpasch  28921  axcontlem4  28947  1pthon2v  30135  mhmimasplusg  33026  cvmlift2lem10  35377  br4  35823  cgrcomim  36054  btwnintr  36084  btwnouttr2  36087  btwndiff  36092  btwnconn1lem14  36165  btwnconn3  36168  segcon2  36170  brsegle  36173  brsegle2  36174  segleantisym  36180  seglelin  36181  outsideofeu  36196  eqlkr  39218  eqlkr2  39219  lkrlsp  39221  atbtwn  39565  athgt  39575  3dimlem3  39580  3dimlem3OLDN  39581  3dim3  39588  3atlem7  39608  4atlem0a  39712  4atlem3a  39716  4atlem11  39728  lneq2at  39897  lnatexN  39898  cdlemb  39913  paddasslem6  39944  llnexchb2  39988  lhp2lt  40120  lhpexle2lem  40128  lhpexle3  40131  lhpmcvr3  40144  lhpat3  40165  ltrnnidn  40293  ltrneq3  40327  cdleme17b  40406  cdleme25a  40472  cdleme25dN  40475  cdleme27cl  40485  cdlemefrs29bpre0  40515  cdlemefs32sn1aw  40533  cdleme32le  40566  cdleme46f2g2  40612  cdleme46f2g1  40613  cdleme50trn3  40672  trlord  40688  ltrniotavalbN  40703  cdlemg6  40742  cdlemg7N  40745  cdlemg11b  40761  cdlemg15a  40774  cdlemg15  40775  cdlemg39  40835  trlcone  40847  cdlemg42  40848  tendoconid  40948  tendotr  40949  cdlemk39u  41087  cdlemk19u  41089  cdleml5N  41099  cdlemm10N  41237  dihord11b  41341  dihord2pre  41344  dihvalcqpre  41354  dihopelvalcpre  41367  dihord6apre  41375  dihord4  41377  dihord5b  41378  dihglblem5apreN  41410  dihmeetlem13N  41438  dihmeetlem19N  41444  dih1dimatlem0  41447  qirropth  43025  mzpcong  43089  jm2.25lem1  43115  jm2.26  43119  idomsubgmo  43310  fourierdlem42  46271  fourierdlem97  46325  clnbgrgrimlem  48057  line2  48877  itscnhlinecirc02plem2  48908