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 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  soisores  7324  frrlem4  8274  omopth2  8584  ttrcltr  9711  fin23lem11  10312  dedekind  11377  xaddass  13228  swrdsbslen  14614  swrdspsleq  14615  ntrivcvgmul  15848  pockthg  16839  gsumsgrpccat  18721  efgred  19616  decpmatmullem  22273  decpmatmul  22274  unconn  22933  basqtop  23215  utop2nei  23755  ucncn  23790  cxple2  26205  cxple2a  26207  nogesgn1ores  27177  nolt02o  27198  nogt01o  27199  nosupbnd1lem1  27211  nosupbnd1lem3  27213  nosupbnd1lem4  27214  nosupbnd1lem5  27215  noinfbnd1lem1  27226  noinfbnd1lem3  27228  noinfbnd1lem4  27229  noinfbnd1lem5  27230  noetalem1  27244  cofcut1  27409  ax5seglem1  28217  ax5seglem2  28218  axpasch  28230  axcontlem4  28256  1pthon2v  29437  cvmlift2lem10  34334  br4  34759  cgrcomim  34992  btwnintr  35022  btwnouttr2  35025  btwndiff  35030  btwnconn1lem14  35103  btwnconn3  35106  segcon2  35108  brsegle  35111  brsegle2  35112  segleantisym  35118  seglelin  35119  outsideofeu  35134  eqlkr  38017  eqlkr2  38018  lkrlsp  38020  atbtwn  38365  athgt  38375  3dimlem3  38380  3dimlem3OLDN  38381  3dim3  38388  3atlem7  38408  4atlem0a  38512  4atlem3a  38516  4atlem11  38528  lneq2at  38697  lnatexN  38698  cdlemb  38713  paddasslem6  38744  llnexchb2  38788  lhp2lt  38920  lhpexle2lem  38928  lhpexle3  38931  lhpmcvr3  38944  lhpat3  38965  ltrnnidn  39093  ltrneq3  39127  cdleme17b  39206  cdleme25a  39272  cdleme25dN  39275  cdleme27cl  39285  cdlemefrs29bpre0  39315  cdlemefs32sn1aw  39333  cdleme32le  39366  cdleme46f2g2  39412  cdleme46f2g1  39413  cdleme50trn3  39472  trlord  39488  ltrniotavalbN  39503  cdlemg6  39542  cdlemg7N  39545  cdlemg11b  39561  cdlemg15a  39574  cdlemg15  39575  cdlemg39  39635  trlcone  39647  cdlemg42  39648  tendoconid  39748  tendotr  39749  cdlemk39u  39887  cdlemk19u  39889  cdleml5N  39899  cdlemm10N  40037  dihord11b  40141  dihord2pre  40144  dihvalcqpre  40154  dihopelvalcpre  40167  dihord6apre  40175  dihord4  40177  dihord5b  40178  dihglblem5apreN  40210  dihmeetlem13N  40238  dihmeetlem19N  40244  dih1dimatlem0  40247  qirropth  41694  mzpcong  41759  jm2.25lem1  41785  jm2.26  41789  idomsubgmo  41988  fourierdlem42  44913  fourierdlem97  44967  line2  47486  itscnhlinecirc02plem2  47517