Theorem simprr3 1225

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

Assertion

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

Proof of Theorem simprr3

Step	Hyp	Ref	Expression
1		simp3 1140	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antll 729	1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  el2xptp0  7786  icodiamlt  14964  psgnunilem2  18841  srgbinom  19514  psgndiflemA  20517  haust1  22203  cnhaus  22205  isreg2  22228  llynlly  22328  restnlly  22333  llyrest  22336  llyidm  22339  nllyidm  22340  cldllycmp  22346  txlly  22487  txnlly  22488  pthaus  22489  txhaus  22498  txkgen  22503  xkohaus  22504  xkococnlem  22510  cmetcaulem  24139  itg2add  24611  ulmdvlem3  25248  ax5seglem6  26979  fusgrfis  27372  wwlksnextfun  27936  umgr2wlkon  27988  connpconn  32864  cvmlift3lem2  32949  cvmlift3lem8  32955  poxp2  33470  nosupprefixmo  33589  noinfprefixmo  33590  nosupno  33592  noinfno  33607  etasslt  33693  scutbdaybnd  33695  scutbdaybnd2  33696  ifscgr  34032  broutsideof3  34114  unblimceq0  34373  paddasslem10  37529  lhpexle2lem  37709  lhpexle3lem  37711  mpaaeu  40619  stoweidlem35  43194  stoweidlem56  43215  stoweidlem59  43218