Theorem simprr2 1229

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

Assertion

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

Proof of Theorem simprr2

Step	Hyp	Ref	Expression
1		simp2 1143	. 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:  poxp2  8090  icodiamlt  15398  psgnunilem2  19468  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  etaslts  27810  cutbdaybnd  27812  cutbdaybnd2  27813  addsproplem6  27991  negsproplem6  28050  mulsproplem13  28145  mulsproplem14  28146  mulsprop  28147  bdayfinbndlem1  28484  ax5seglem6  29028  n4cyclfrgr  30386  connpconn  35470  cvmlift3lem2  35555  cvmlift3lem8  35561  broutsideof3  36361  unblimceq0  36820  paddasslem10  40328  lhpexle2lem  40508  lhpexle3lem  40510  stoweidlem35  46485  stoweidlem56  46506  stoweidlem59  46509  pgn4cyclex  48624  2arwcat  50097