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  8187  sqrmo  15447  icodiamlt  15634  psgnunilem2  19739  haust1  23700  cnhaus  23702  isreg2  23725  llynlly  23826  restnlly  23831  llyrest  23834  llyidm  23837  nllyidm  23838  cldllycmp  23844  txlly  23985  txnlly  23986  pthaus  23987  txhaus  23996  txkgen  24001  xkohaus  24002  xkococnlem  24008  hauspwpwf1  24336  itg2add  26110  ulmdvlem3  26759  nosupno  28090  noinfno  28105  etaslts  28209  cutbdaybnd  28211  cutbdaybnd2  28212  addsproplem6  28390  negsproplem6  28449  mulsproplem13  28544  mulsproplem14  28545  mulsprop  28546  bdayfinbndlem1  28883  ax5seglem6  29542  fusgrfis  29941  umgr2wlkon  30569  numclwwlk5  31019  connpconn  36167  cvmliftmolem2  36214  cvmlift2lem10  36244  cvmlift3lem2  36252  cvmlift3lem8  36258  broutsideof3  37069  unblimceq0  37551  paddasslem10  41078  lhpexle2lem  41258  lhpexle3lem  41260  cdlemj3  42072  cdlemkid4  42183  mpaaeu  44344  stoweidlem35  47250  stoweidlem56  47271  stoweidlem59  47274  2arwcat  50943