Theorem simplr1 1217

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simplr1	⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑)

Proof of Theorem simplr1

Step	Hyp	Ref	Expression
1		simp1 1137	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antlr 728	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  soltmin  6099  frfi  9195  wemappo  9464  iccsplit  13438  ccatswrd  14631  sqrmo  15213  pcdvdstr  16847  vdwlem12  16963  mreexexlem4d  17613  iscatd2  17647  oppccomfpropd  17693  resssetc  18059  resscatc  18076  mod1ile  18459  mod2ile  18460  prdssgrpd  18701  prdsmndd  18738  grprcan  18949  submomnd  20107  ogrpaddltbi  20114  prdsrngd  20157  prdsringd  20300  lmodprop2d  20919  lssintcl  20959  prdslmodd  20964  islmhm2  21033  islbs3  21153  ofco2  22416  mdetmul  22588  restopnb  23140  regsep2  23341  iunconn  23393  blsscls2  24469  met2ndci  24487  xrsblre  24777  nosupbnd1lem5  27676  conway  27771  addsass  27997  mulscom  28131  legso  28667  colline  28717  tglowdim2ln  28719  cgrahl  28895  f1otrg  28939  f1otrge  28940  ax5seglem4  29001  ax5seglem5  29002  axcontlem4  29036  axcontlem8  29040  axcontlem9  29041  axcontlem10  29042  eengtrkg  29055  rusgrnumwwlks  30045  frgr3v  30345  lmhmimasvsca  33099  erdszelem8  35380  elmrsubrn  35702  btwncomim  36195  btwnswapid  36199  broutsideof3  36308  outsideoftr  36311  outsidele  36314  isbasisrelowllem1  37671  isbasisrelowllem2  37672  cvrletrN  39719  ltltncvr  39869  atcvrj2b  39878  2at0mat0  39971  paddasslem11  40276  pmod1i  40294  lautcvr  40538  tendoplass  41229  tendodi1  41230  tendodi2  41231  cdlemk34  41356  mendassa  43618  grumnud  44713  3adantlr3  45471  ssinc  45517  ssdec  45518  ioondisj2  45923  ioondisj1  45924  subsubelfzo0  47775  ply1mulgsumlem2  48863  lincresunit3lem2  48956  catprs  49486  fthcomf  49632  oppcthinco  49914  oppcthinendcALT  49916