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  8015  poxp2  8122  ttrcltr  9669  icodiamlt  15404  psgnunilem2  19425  srgbinom  20140  psgndiflemA  21510  haust1  23239  cnhaus  23241  isreg2  23264  llynlly  23364  restnlly  23369  llyrest  23372  llyidm  23375  nllyidm  23376  cldllycmp  23382  txlly  23523  txnlly  23524  pthaus  23525  txhaus  23534  txkgen  23539  xkohaus  23540  xkococnlem  23546  cmetcaulem  25188  itg2add  25660  ulmdvlem3  26311  nosupprefixmo  27612  noinfprefixmo  27613  nosupno  27615  noinfno  27630  etasslt  27725  scutbdaybnd  27727  scutbdaybnd2  27728  addsproplem6  27881  negsproplem6  27939  mulsproplem13  28031  mulsproplem14  28032  mulsprop  28033  ax5seglem6  28861  fusgrfis  29257  wwlksnextfun  29828  umgr2wlkon  29880  connpconn  35222  cvmlift3lem2  35307  cvmlift3lem8  35313  ifscgr  36032  broutsideof3  36114  unblimceq0  36495  paddasslem10  39823  lhpexle2lem  40003  lhpexle3lem  40005  mpaaeu  43139  stoweidlem35  46033  stoweidlem56  46054  stoweidlem59  46057  2arwcat  49589