Theorem simprr3 1224

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  el2xptp0  8040  poxp2  8147  ttrcltr  9735  icodiamlt  15459  psgnunilem2  19481  srgbinom  20196  psgndiflemA  21566  haust1  23295  cnhaus  23297  isreg2  23320  llynlly  23420  restnlly  23425  llyrest  23428  llyidm  23431  nllyidm  23432  cldllycmp  23438  txlly  23579  txnlly  23580  pthaus  23581  txhaus  23590  txkgen  23595  xkohaus  23596  xkococnlem  23602  cmetcaulem  25245  itg2add  25717  ulmdvlem3  26368  nosupprefixmo  27669  noinfprefixmo  27670  nosupno  27672  noinfno  27687  etasslt  27782  scutbdaybnd  27784  scutbdaybnd2  27785  addsproplem6  27938  negsproplem6  27996  mulsproplem13  28088  mulsproplem14  28089  mulsprop  28090  ax5seglem6  28918  fusgrfis  29314  wwlksnextfun  29885  umgr2wlkon  29937  connpconn  35262  cvmlift3lem2  35347  cvmlift3lem8  35353  ifscgr  36067  broutsideof3  36149  unblimceq0  36530  paddasslem10  39853  lhpexle2lem  40033  lhpexle3lem  40035  mpaaeu  43141  stoweidlem35  46031  stoweidlem56  46052  stoweidlem59  46055  2arwcat  49444