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  6134  frfi  9259  wemappo  9525  iccsplit  13542  ccatswrd  14742  pcdvdstr  16974  vdwlem12  17090  iscatd2  17775  oppccomfpropd  17821  resssetc  18187  resscatc  18204  mod1ile  18587  mod2ile  18588  prdssgrpd  18841  prdsmndd  18883  grprcan  19103  mulgnn0dir  19233  mulgnn0di  19958  mulgdi  19959  submomnd  20265  ogrpaddltbi  20272  lmodprop2d  21114  lssintcl  21154  prdslmodd  21159  islmhm2  21228  islbs3  21348  mdetmul  22851  restopnb  23406  nrmsep  23588  iunconn  23659  ptpjopn  23844  blsscls2  24736  xrsblre  25044  icccmplem2  25056  icccvx  25184  conway  28052  addsass  28278  mulscom  28412  addonbday  28552  colline  29005  tglowdim2ln  29007  f1otrg  29335  f1otrge  29336  ax5seglem5  29398  axcontlem3  29431  axcontlem4  29432  axcontlem8  29436  eengtrkg  29451  2pthon3v  30419  erclwwlktr  30500  erclwwlkntr  30549  eucrctshift  30731  frgr3v  30763  frgr2wwlkeqm  30819  xrofsup  33246  lmhmimasvsca  33486  erdszelem8  35785  cvmliftmolem2  35869  cvmlift2lem12  35901  r1peuqusdeg1  36230  btwnswapid  36605  btwnsegle  36705  broutsideof3  36714  outsidele  36720  nmulprop  36778  nmulcom  36782  isbasisrelowllem2  38118  cvrletrN  40154  ltltncvr  40304  atcvrj2b  40313  cvrat4  40324  2at0mat0  40406  islpln2a  40429  paddasslem11  40711  pmod1i  40729  lautcvr  40973  cdlemg4c  41493  tendoplass  41664  tendodi1  41665  tendodi2  41666  mendlmod  44038  mendassa  44039  3adantlr3  45882  ssinc  45927  ssdec  45928  ioondisj2  46331  ioondisj1  46332  stoweidlem60  46896  ply1mulgsumlem2  49325  lincresunit3lem2  49418  catprs  49945  fthcomf  50091  oppcthinco  50373  oppcthinendcALT  50375