Theorem simplr1 1234

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 1154	. 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  sqrmo  15398  pcdvdstr  17034  vdwlem12  17150  mreexexlem4d  17801  iscatd2  17835  oppccomfpropd  17881  resssetc  18247  resscatc  18264  mod1ile  18647  mod2ile  18648  prdssgrpd  18902  prdsmndd  18944  grprcan  19164  submomnd  20326  ogrpaddltbi  20333  prdsrngd  20378  prdsringd  20530  lmodprop2d  21179  lssintcl  21219  prdslmodd  21224  islmhm2  21293  islbs3  21413  ofco2  22746  mdetmul  22918  restopnb  23473  regsep2  23674  iunconn  23726  blsscls2  24803  met2ndci  24821  xrsblre  25111  nosupbnd1lem5  28051  conway  28147  addsass  28373  mulscom  28507  legso  29044  colline  29100  tglowdim2ln  29102  cgrahl  29317  f1otrg  29430  f1otrge  29431  ax5seglem4  29492  ax5seglem5  29493  axcontlem4  29527  axcontlem8  29531  axcontlem9  29532  axcontlem10  29533  eengtrkg  29546  rusgrnumwwlks  30548  frgr3v  30858  lmhmimasvsca  33581  erdszelem8  35932  elmrsubrn  36254  btwncomim  36748  btwnswapid  36752  broutsideof3  36861  outsideoftr  36864  outsidele  36867  nmulprop  36909  nmulcom  36913  isbasisrelowllem1  38246  isbasisrelowllem2  38247  cvrletrN  40298  ltltncvr  40448  atcvrj2b  40457  2at0mat0  40550  paddasslem11  40855  pmod1i  40873  lautcvr  41117  tendoplass  41808  tendodi1  41809  tendodi2  41810  cdlemk34  41935  mendassa  44150  grumnud  45229  3adantlr3  46000  ssinc  46045  ssdec  46046  ioondisj2  46449  ioondisj1  46450  tmachlem-franscan  47903  subsubelfzo0  48341  ply1mulgsumlem2  49443  lincresunit3lem2  49536  catprs  50063  fthcomf  50209  oppcthinco  50491  oppcthinendcALT  50493