Theorem simplr1 1216

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 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  6109  frfi  9232  wemappo  9502  iccsplit  13446  ccatswrd  14633  sqrmo  15217  pcdvdstr  16847  vdwlem12  16963  mreexexlem4d  17608  iscatd2  17642  oppccomfpropd  17688  resssetc  18054  resscatc  18071  mod1ile  18452  mod2ile  18453  prdssgrpd  18660  prdsmndd  18697  grprcan  18905  prdsrngd  20085  prdsringd  20230  lmodprop2d  20830  lssintcl  20870  prdslmodd  20875  islmhm2  20945  islbs3  21065  ofco2  22338  mdetmul  22510  restopnb  23062  regsep2  23263  iunconn  23315  blsscls2  24392  met2ndci  24410  xrsblre  24700  nosupbnd1lem5  27624  conway  27711  addsass  27912  mulscom  28042  legso  28526  colline  28576  tglowdim2ln  28578  cgrahl  28754  f1otrg  28798  f1otrge  28799  ax5seglem4  28859  ax5seglem5  28860  axcontlem4  28894  axcontlem8  28898  axcontlem9  28899  axcontlem10  28900  eengtrkg  28913  rusgrnumwwlks  29904  frgr3v  30204  lmhmimasvsca  32980  submomnd  33024  ogrpaddltbi  33032  erdszelem8  35185  elmrsubrn  35507  btwncomim  36001  btwnswapid  36005  broutsideof3  36114  outsideoftr  36117  outsidele  36120  isbasisrelowllem1  37343  isbasisrelowllem2  37344  cvrletrN  39266  ltltncvr  39417  atcvrj2b  39426  2at0mat0  39519  paddasslem11  39824  pmod1i  39842  lautcvr  40086  tendoplass  40777  tendodi1  40778  tendodi2  40779  cdlemk34  40904  mendassa  43179  grumnud  44275  3adantlr3  45034  ssinc  45081  ssdec  45082  ioondisj2  45491  ioondisj1  45492  subsubelfzo0  47327  ply1mulgsumlem2  48376  lincresunit3lem2  48469  catprs  49000  fthcomf  49146  oppcthinco  49428  oppcthinendcALT  49430