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  7320  frrlem4  8288  omopth2  8596  ttrcltr  9730  fin23lem11  10331  dedekind  11398  xaddass  13265  swrdsbslen  14682  swrdspsleq  14683  ntrivcvgmul  15918  pockthg  16926  gsumsgrpccat  18818  efgred  19729  decpmatmullem  22709  decpmatmul  22710  unconn  23367  basqtop  23649  utop2nei  24189  ucncn  24223  cxple2  26658  cxple2a  26660  nogesgn1ores  27638  nolt02o  27659  nogt01o  27660  nosupbnd1lem1  27672  nosupbnd1lem3  27674  nosupbnd1lem4  27675  nosupbnd1lem5  27676  noinfbnd1lem1  27687  noinfbnd1lem3  27689  noinfbnd1lem4  27690  noinfbnd1lem5  27691  noetalem1  27705  cofcut1  27880  ax5seglem1  28907  ax5seglem2  28908  axpasch  28920  axcontlem4  28946  1pthon2v  30134  mhmimasplusg  33033  cvmlift2lem10  35334  br4  35775  cgrcomim  36007  btwnintr  36037  btwnouttr2  36040  btwndiff  36045  btwnconn1lem14  36118  btwnconn3  36121  segcon2  36123  brsegle  36126  brsegle2  36127  segleantisym  36133  seglelin  36134  outsideofeu  36149  eqlkr  39117  eqlkr2  39118  lkrlsp  39120  atbtwn  39465  athgt  39475  3dimlem3  39480  3dimlem3OLDN  39481  3dim3  39488  3atlem7  39508  4atlem0a  39612  4atlem3a  39616  4atlem11  39628  lneq2at  39797  lnatexN  39798  cdlemb  39813  paddasslem6  39844  llnexchb2  39888  lhp2lt  40020  lhpexle2lem  40028  lhpexle3  40031  lhpmcvr3  40044  lhpat3  40065  ltrnnidn  40193  ltrneq3  40227  cdleme17b  40306  cdleme25a  40372  cdleme25dN  40375  cdleme27cl  40385  cdlemefrs29bpre0  40415  cdlemefs32sn1aw  40433  cdleme32le  40466  cdleme46f2g2  40512  cdleme46f2g1  40513  cdleme50trn3  40572  trlord  40588  ltrniotavalbN  40603  cdlemg6  40642  cdlemg7N  40645  cdlemg11b  40661  cdlemg15a  40674  cdlemg15  40675  cdlemg39  40735  trlcone  40747  cdlemg42  40748  tendoconid  40848  tendotr  40849  cdlemk39u  40987  cdlemk19u  40989  cdleml5N  40999  cdlemm10N  41137  dihord11b  41241  dihord2pre  41244  dihvalcqpre  41254  dihopelvalcpre  41267  dihord6apre  41275  dihord4  41277  dihord5b  41278  dihglblem5apreN  41310  dihmeetlem13N  41338  dihmeetlem19N  41344  dih1dimatlem0  41347  qirropth  42931  mzpcong  42996  jm2.25lem1  43022  jm2.26  43026  idomsubgmo  43217  fourierdlem42  46178  fourierdlem97  46232  clnbgrgrimlem  47946  line2  48732  itscnhlinecirc02plem2  48763