Theorem simprr1 1240

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simprr1	⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑)

Proof of Theorem simprr1

Step	Hyp	Ref	Expression
1		simp1 1154	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antll 742	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:  poxp2  8162  sqrmo  15423  icodiamlt  15610  psgnunilem2  19714  haust1  23675  cnhaus  23677  isreg2  23700  llynlly  23801  restnlly  23806  llyrest  23809  llyidm  23812  nllyidm  23813  cldllycmp  23819  txlly  23960  txnlly  23961  pthaus  23962  txhaus  23971  txkgen  23976  xkohaus  23977  xkococnlem  23983  hauspwpwf1  24311  itg2add  26085  ulmdvlem3  26734  nosupno  28065  noinfno  28080  etaslts  28184  cutbdaybnd  28186  cutbdaybnd2  28187  addsproplem6  28365  negsproplem6  28424  mulsproplem13  28519  mulsproplem14  28520  mulsprop  28521  bdayfinbndlem1  28858  ax5seglem6  29517  fusgrfis  29916  umgr2wlkon  30544  numclwwlk5  30994  connpconn  36086  cvmliftmolem2  36133  cvmlift2lem10  36163  cvmlift3lem2  36171  cvmlift3lem8  36177  broutsideof3  36983  unblimceq0  37465  paddasslem10  40979  lhpexle2lem  41159  lhpexle3lem  41161  cdlemj3  41973  cdlemkid4  42084  mpaaeu  44245  stoweidlem35  47138  stoweidlem56  47159  stoweidlem59  47162  2arwcat  50831