Theorem simpl2l 1245

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  soisores  7327  frrlem4  8287  omopth2  8570  ttrcltr  9686  fin23lem11  10302  dedekind  11374  xaddass  13276  swrdsbslen  14704  swrdspsleq  14705  ntrivcvgmul  15958  pockthg  16967  gsumsgrpccat  18900  efgred  19819  decpmatmullem  22909  decpmatmul  22910  unconn  23567  basqtop  23849  utop2nei  24388  ucncn  24422  cxple2  26840  cxple2a  26842  nogesgn1ores  27816  nolt02o  27837  nogt01o  27838  nosupbnd1lem1  27850  nosupbnd1lem3  27852  nosupbnd1lem4  27853  nosupbnd1lem5  27854  noinfbnd1lem1  27865  noinfbnd1lem3  27867  noinfbnd1lem4  27868  noinfbnd1lem5  27869  noetalem1  27883  cofcut1  28091  bdayfinbndlem1  28638  ax5seglem1  29256  ax5seglem2  29257  axpasch  29269  axcontlem4  29295  1pthon2v  30482  mhmimasplusg  33335  cvmlift2lem10  35782  br4  36228  cgrcomim  36459  btwnintr  36489  btwnouttr2  36492  btwndiff  36497  btwnconn1lem14  36570  btwnconn3  36573  segcon2  36575  brsegle  36578  brsegle2  36579  segleantisym  36585  seglelin  36586  outsideofeu  36601  eqlkr  39851  eqlkr2  39852  lkrlsp  39854  atbtwn  40198  athgt  40208  3dimlem3  40213  3dimlem3OLDN  40214  3dim3  40221  3atlem7  40241  4atlem0a  40345  4atlem3a  40349  4atlem11  40361  lneq2at  40530  lnatexN  40531  cdlemb  40546  paddasslem6  40577  llnexchb2  40621  lhp2lt  40753  lhpexle2lem  40761  lhpexle3  40764  lhpmcvr3  40777  lhpat3  40798  ltrnnidn  40926  ltrneq3  40960  cdleme17b  41039  cdleme25a  41105  cdleme25dN  41108  cdleme27cl  41118  cdlemefrs29bpre0  41148  cdlemefs32sn1aw  41166  cdleme32le  41199  cdleme46f2g2  41245  cdleme46f2g1  41246  cdleme50trn3  41305  trlord  41321  ltrniotavalbN  41336  cdlemg6  41375  cdlemg7N  41378  cdlemg11b  41394  cdlemg15a  41407  cdlemg15  41408  cdlemg39  41468  trlcone  41480  cdlemg42  41481  tendoconid  41581  tendotr  41582  cdlemk39u  41720  cdlemk19u  41722  cdleml5N  41732  cdlemm10N  41870  dihord11b  41974  dihord2pre  41977  dihvalcqpre  41987  dihopelvalcpre  42000  dihord6apre  42008  dihord4  42010  dihord5b  42011  dihglblem5apreN  42043  dihmeetlem13N  42071  dihmeetlem19N  42077  dih1dimatlem0  42080  qirropth  43615  mzpcong  43679  jm2.25lem1  43705  jm2.26  43709  idomsubgmo  43900  fourierdlem42  46843  fourierdlem97  46897  clnbgrgrimlem  48675  line2  49509  itscnhlinecirc02plem2  49540