Theorem simp-4l 770

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)

Assertion

Ref	Expression
simp-4l	⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Proof of Theorem simp-4l

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜑 → 𝜑)
2	1	ad4antr 719	1 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  marypha1lem  8692  acndom2  9274  ttukeylem6  9734  fpwwe2lem12  9861  reuccats1OLD  13921  dfgcd2  15750  ramcl  16221  initoeu2lem1  17132  initoeu2  17134  gsmsymgreqlem2  18320  dfod2  18452  pgpfi  18491  ghmcyg  18770  psgndif  20448  scmatmulcl  20831  cpmatmcllem  21030  neiptoptop  21443  cncnp  21592  subislly  21793  ptcnplem  21933  pthaus  21950  xkohaus  21965  kqreglem1  22053  cnextcn  22379  qustgplem  22432  trust  22541  utoptop  22546  restutopopn  22550  utop3cls  22563  utopreg  22564  isucn2  22591  met1stc  22834  metustsym  22868  metuel2  22878  xrge0tsms  23145  xmetdcn2  23148  nmoleub2lem2  23423  iscfil2  23572  iscfil3  23579  dvmptfsum  24275  dvlip2  24295  aannenlem1  24620  ulm2  24676  ulmuni  24683  mtestbdd  24696  efopn  24942  dchrptlem1  25542  pntpbnd  25866  pntibnd  25871  f1otrg  26360  nbupgr  26829  upgriswlk  27125  usgr2pth  27253  clwlkclwwlklem2a4  27503  cusconngr  27720  xrofsup  30251  ressprs  30380  omndmul2  30437  isarchi3  30488  archirngz  30490  lmodslmd  30504  gsummpt2d  30530  xrge0tsmsd  30536  suborng  30573  isarchiofld  30575  dimkerim  30658  sqsscirc1  30801  lmxrge0  30845  lmdvg  30846  esumrnmpt2  30977  esumfsup  30979  esumcvg  30995  esum2d  31002  ddemeas  31146  omssubadd  31209  noetalem3  32746  btwnconn1lem13  33087  matunitlindflem1  34335  matunitlindflem2  34336  poimirlem29  34368  mblfinlem3  34378  mblfinlem4  34379  ftc1anclem7  34420  ftc1anc  34422  prdstotbnd  34520  ltrnid  36722  rencldnfilem  38819  pellex  38834  pellfundex  38885  dvdsacongtr  38983  fnchoice  40711  climsuse  41326  addlimc  41366  0ellimcdiv  41367  climxrre  41468  xlimmnfvlem2  41551  xlimpnfvlem2  41555  icccncfext  41606  dvnprodlem3  41669  fourierdlem12  41841  fourierdlem34  41863  fourierdlem50  41878  fourierdlem80  41908  fourierdlem81  41909  fourierdlem87  41915  etransclem35  41991  sge0pr  42113  meaiuninc3v  42203  smfmullem3  42505  mogoldbb  43324  uzlidlring  43570  2zlidl  43575