Theorem simplr2 1217

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

Assertion

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

Proof of Theorem simplr2

Step	Hyp	Ref	Expression
1		simp2 1137	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antlr 727	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:  soltmin  6109  frfi  9232  wemappo  9502  iccsplit  13446  ccatswrd  14633  pcdvdstr  16847  vdwlem12  16963  iscatd2  17642  oppccomfpropd  17688  resssetc  18054  resscatc  18071  mod1ile  18452  mod2ile  18453  prdssgrpd  18660  prdsmndd  18697  grprcan  18905  mulgnn0dir  19036  mulgnn0di  19755  mulgdi  19756  lmodprop2d  20830  lssintcl  20870  prdslmodd  20875  islmhm2  20945  islbs3  21065  mdetmul  22510  restopnb  23062  nrmsep  23244  iunconn  23315  ptpjopn  23499  blsscls2  24392  xrsblre  24700  icccmplem2  24712  icccvx  24848  conway  27711  addsass  27912  mulscom  28042  colline  28576  tglowdim2ln  28578  f1otrg  28798  f1otrge  28799  ax5seglem5  28860  axcontlem3  28893  axcontlem4  28894  axcontlem8  28898  eengtrkg  28913  2pthon3v  29873  erclwwlktr  29951  erclwwlkntr  30000  eucrctshift  30172  frgr3v  30204  frgr2wwlkeqm  30260  xrofsup  32690  lmhmimasvsca  32980  submomnd  33024  ogrpaddltbi  33032  erdszelem8  35185  cvmliftmolem2  35269  cvmlift2lem12  35301  r1peuqusdeg1  35630  btwnswapid  36005  btwnsegle  36105  broutsideof3  36114  outsidele  36120  isbasisrelowllem2  37344  cvrletrN  39266  ltltncvr  39417  atcvrj2b  39426  cvrat4  39437  2at0mat0  39519  islpln2a  39542  paddasslem11  39824  pmod1i  39842  lautcvr  40086  cdlemg4c  40606  tendoplass  40777  tendodi1  40778  tendodi2  40779  mendlmod  43178  mendassa  43179  3adantlr3  45034  ssinc  45081  ssdec  45082  ioondisj2  45491  ioondisj1  45492  stoweidlem60  46058  ply1mulgsumlem2  48376  lincresunit3lem2  48469  catprs  49000  fthcomf  49146  oppcthinco  49428  oppcthinendcALT  49430