Theorem simplr2 1235

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 1155	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antlr 740	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  soltmin  6128  frfi  9260  wemappo  9527  iccsplit  13597  ccatswrd  14798  pcdvdstr  17034  vdwlem12  17150  iscatd2  17835  oppccomfpropd  17881  resssetc  18247  resscatc  18264  mod1ile  18647  mod2ile  18648  prdssgrpd  18902  prdsmndd  18944  grprcan  19164  mulgnn0dir  19294  mulgnn0di  20019  mulgdi  20020  submomnd  20326  ogrpaddltbi  20333  lmodprop2d  21179  lssintcl  21219  prdslmodd  21224  islmhm2  21293  islbs3  21413  mdetmul  22918  restopnb  23473  nrmsep  23655  iunconn  23726  ptpjopn  23911  blsscls2  24803  xrsblre  25111  icccmplem2  25123  icccvx  25251  conway  28147  addsass  28373  mulscom  28507  addonbday  28647  colline  29100  tglowdim2ln  29102  f1otrg  29430  f1otrge  29431  ax5seglem5  29493  axcontlem3  29526  axcontlem4  29527  axcontlem8  29531  eengtrkg  29546  2pthon3v  30514  erclwwlktr  30595  erclwwlkntr  30644  eucrctshift  30826  frgr3v  30858  frgr2wwlkeqm  30914  xrofsup  33341  lmhmimasvsca  33581  erdszelem8  35932  cvmliftmolem2  36016  cvmlift2lem12  36048  r1peuqusdeg1  36377  btwnswapid  36752  btwnsegle  36852  broutsideof3  36861  outsidele  36867  nmulprop  36909  nmulcom  36913  isbasisrelowllem2  38247  cvrletrN  40298  ltltncvr  40448  atcvrj2b  40457  cvrat4  40468  2at0mat0  40550  islpln2a  40573  paddasslem11  40855  pmod1i  40873  lautcvr  41117  cdlemg4c  41637  tendoplass  41808  tendodi1  41809  tendodi2  41810  mendlmod  44149  mendassa  44150  3adantlr3  46000  ssinc  46045  ssdec  46046  ioondisj2  46449  ioondisj1  46450  stoweidlem60  47014  ply1mulgsumlem2  49443  lincresunit3lem2  49536  catprs  50063  fthcomf  50209  oppcthinco  50491  oppcthinendcALT  50493