Theorem simplr1 1215

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 725	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1087

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 206  df-an 398  df-3an 1089

This theorem is referenced by:  soltmin  6056  frfi  9103  wemappo  9352  iccsplit  13263  ccatswrd  14426  sqrmo  15008  pcdvdstr  16622  vdwlem12  16738  mreexexlem4d  17401  iscatd2  17435  oppccomfpropd  17483  resssetc  17852  resscatc  17869  mod1ile  18256  mod2ile  18257  prdsmndd  18463  grprcan  18658  prdsringd  19896  lmodprop2d  20230  lssintcl  20271  prdslmodd  20276  islmhm2  20345  islbs3  20462  ofco2  21645  mdetmul  21817  restopnb  22371  regsep2  22572  iunconn  22624  blsscls2  23705  met2ndci  23723  xrsblre  24019  legso  27005  colline  27055  tglowdim2ln  27057  cgrahl  27233  f1otrg  27277  f1otrge  27278  ax5seglem4  27345  ax5seglem5  27346  axcontlem4  27380  axcontlem8  27384  axcontlem9  27385  axcontlem10  27386  eengtrkg  27399  rusgrnumwwlks  28384  frgr3v  28684  submomnd  31381  ogrpaddltbi  31389  erdszelem8  33205  elmrsubrn  33527  nosupbnd1lem5  33960  conway  34038  btwncomim  34360  btwnswapid  34364  broutsideof3  34473  outsideoftr  34476  outsidele  34479  isbasisrelowllem1  35570  isbasisrelowllem2  35571  cvrletrN  37329  ltltncvr  37479  atcvrj2b  37488  2at0mat0  37581  paddasslem11  37886  pmod1i  37904  lautcvr  38148  tendoplass  38839  tendodi1  38840  tendodi2  38841  cdlemk34  38966  mendassa  41057  grumnud  41942  3adantlr3  42622  ssinc  42675  ssdec  42676  ioondisj2  43080  ioondisj1  43081  subsubelfzo0  44876  ply1mulgsumlem2  45786  lincresunit3lem2  45879  catprs  46350