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  7305  frrlem4  8271  omopth2  8551  ttrcltr  9676  fin23lem11  10277  dedekind  11344  xaddass  13216  swrdsbslen  14636  swrdspsleq  14637  ntrivcvgmul  15875  pockthg  16884  gsumsgrpccat  18774  efgred  19685  decpmatmullem  22665  decpmatmul  22666  unconn  23323  basqtop  23605  utop2nei  24145  ucncn  24179  cxple2  26613  cxple2a  26615  nogesgn1ores  27593  nolt02o  27614  nogt01o  27615  nosupbnd1lem1  27627  nosupbnd1lem3  27629  nosupbnd1lem4  27630  nosupbnd1lem5  27631  noinfbnd1lem1  27642  noinfbnd1lem3  27644  noinfbnd1lem4  27645  noinfbnd1lem5  27646  noetalem1  27660  cofcut1  27835  ax5seglem1  28862  ax5seglem2  28863  axpasch  28875  axcontlem4  28901  1pthon2v  30089  mhmimasplusg  32986  cvmlift2lem10  35306  br4  35752  cgrcomim  35984  btwnintr  36014  btwnouttr2  36017  btwndiff  36022  btwnconn1lem14  36095  btwnconn3  36098  segcon2  36100  brsegle  36103  brsegle2  36104  segleantisym  36110  seglelin  36111  outsideofeu  36126  eqlkr  39099  eqlkr2  39100  lkrlsp  39102  atbtwn  39447  athgt  39457  3dimlem3  39462  3dimlem3OLDN  39463  3dim3  39470  3atlem7  39490  4atlem0a  39594  4atlem3a  39598  4atlem11  39610  lneq2at  39779  lnatexN  39780  cdlemb  39795  paddasslem6  39826  llnexchb2  39870  lhp2lt  40002  lhpexle2lem  40010  lhpexle3  40013  lhpmcvr3  40026  lhpat3  40047  ltrnnidn  40175  ltrneq3  40209  cdleme17b  40288  cdleme25a  40354  cdleme25dN  40357  cdleme27cl  40367  cdlemefrs29bpre0  40397  cdlemefs32sn1aw  40415  cdleme32le  40448  cdleme46f2g2  40494  cdleme46f2g1  40495  cdleme50trn3  40554  trlord  40570  ltrniotavalbN  40585  cdlemg6  40624  cdlemg7N  40627  cdlemg11b  40643  cdlemg15a  40656  cdlemg15  40657  cdlemg39  40717  trlcone  40729  cdlemg42  40730  tendoconid  40830  tendotr  40831  cdlemk39u  40969  cdlemk19u  40971  cdleml5N  40981  cdlemm10N  41119  dihord11b  41223  dihord2pre  41226  dihvalcqpre  41236  dihopelvalcpre  41249  dihord6apre  41257  dihord4  41259  dihord5b  41260  dihglblem5apreN  41292  dihmeetlem13N  41320  dihmeetlem19N  41326  dih1dimatlem0  41329  qirropth  42903  mzpcong  42968  jm2.25lem1  42994  jm2.26  42998  idomsubgmo  43189  fourierdlem42  46154  fourierdlem97  46208  clnbgrgrimlem  47937  line2  48745  itscnhlinecirc02plem2  48776