Theorem simplr2 1215

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 1136	. 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  6159  frfi  9319  wemappo  9587  iccsplit  13522  ccatswrd  14703  pcdvdstr  16910  vdwlem12  17026  iscatd2  17726  oppccomfpropd  17774  resssetc  18146  resscatc  18163  mod1ile  18551  mod2ile  18552  prdssgrpd  18759  prdsmndd  18796  grprcan  19004  mulgnn0dir  19135  mulgnn0di  19858  mulgdi  19859  lmodprop2d  20939  lssintcl  20980  prdslmodd  20985  islmhm2  21055  islbs3  21175  mdetmul  22645  restopnb  23199  nrmsep  23381  iunconn  23452  ptpjopn  23636  blsscls2  24533  xrsblre  24847  icccmplem2  24859  icccvx  24995  conway  27859  addsass  28053  mulscom  28180  colline  28672  tglowdim2ln  28674  f1otrg  28894  f1otrge  28895  ax5seglem5  28963  axcontlem3  28996  axcontlem4  28997  axcontlem8  29001  eengtrkg  29016  2pthon3v  29973  erclwwlktr  30051  erclwwlkntr  30100  eucrctshift  30272  frgr3v  30304  frgr2wwlkeqm  30360  xrofsup  32778  lmhmimasvsca  33027  submomnd  33070  ogrpaddltbi  33078  erdszelem8  35183  cvmliftmolem2  35267  cvmlift2lem12  35299  r1peuqusdeg1  35628  btwnswapid  35999  btwnsegle  36099  broutsideof3  36108  outsidele  36114  isbasisrelowllem2  37339  cvrletrN  39255  ltltncvr  39406  atcvrj2b  39415  cvrat4  39426  2at0mat0  39508  islpln2a  39531  paddasslem11  39813  pmod1i  39831  lautcvr  40075  cdlemg4c  40595  tendoplass  40766  tendodi1  40767  tendodi2  40768  mendlmod  43178  mendassa  43179  3adantlr3  44978  ssinc  45027  ssdec  45028  ioondisj2  45446  ioondisj1  45447  stoweidlem60  46016  ply1mulgsumlem2  48233  lincresunit3lem2  48326  catprs  48800