Theorem simprr3 1223

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 727	1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒)

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

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  el2xptp0  8024  poxp2  8131  ttrcltr  9713  icodiamlt  15386  psgnunilem2  19404  srgbinom  20125  psgndiflemA  21373  haust1  23076  cnhaus  23078  isreg2  23101  llynlly  23201  restnlly  23206  llyrest  23209  llyidm  23212  nllyidm  23213  cldllycmp  23219  txlly  23360  txnlly  23361  pthaus  23362  txhaus  23371  txkgen  23376  xkohaus  23377  xkococnlem  23383  cmetcaulem  25029  itg2add  25501  ulmdvlem3  26138  nosupprefixmo  27427  noinfprefixmo  27428  nosupno  27430  noinfno  27445  etasslt  27539  scutbdaybnd  27541  scutbdaybnd2  27542  addsproplem6  27684  negsproplem6  27734  mulsproplem13  27811  mulsproplem14  27812  mulsprop  27813  ax5seglem6  28447  fusgrfis  28842  wwlksnextfun  29407  umgr2wlkon  29459  connpconn  34512  cvmlift3lem2  34597  cvmlift3lem8  34603  ifscgr  35308  broutsideof3  35390  unblimceq0  35686  paddasslem10  39003  lhpexle2lem  39183  lhpexle3lem  39185  mpaaeu  42194  stoweidlem35  45050  stoweidlem56  45071  stoweidlem59  45074