Theorem simprr3 1230

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 1144	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antll 735	1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  el2xptp0  7985  poxp2  8090  ttrcltr  9635  icodiamlt  15398  psgnunilem2  19468  srgbinom  20210  psgndiflemA  21583  haust1  23342  cnhaus  23344  isreg2  23367  llynlly  23467  restnlly  23472  llyrest  23475  llyidm  23478  nllyidm  23479  cldllycmp  23485  txlly  23626  txnlly  23627  pthaus  23628  txhaus  23637  txkgen  23642  xkohaus  23643  xkococnlem  23649  cmetcaulem  25280  itg2add  25751  ulmdvlem3  26392  nosupprefixmo  27689  noinfprefixmo  27690  nosupno  27692  noinfno  27707  etaslts  27810  cutbdaybnd  27812  cutbdaybnd2  27813  addsproplem6  27991  negsproplem6  28050  mulsproplem13  28145  mulsproplem14  28146  mulsprop  28147  bdayfinbndlem1  28484  ax5seglem6  29028  fusgrfis  29424  wwlksnextfun  29991  umgr2wlkon  30043  connpconn  35464  cvmlift3lem2  35549  cvmlift3lem8  35555  ifscgr  36273  broutsideof3  36355  unblimceq0  36814  paddasslem10  40322  lhpexle2lem  40502  lhpexle3lem  40504  mpaaeu  43596  stoweidlem35  46479  stoweidlem56  46500  stoweidlem59  46503  2arwcat  50091