Theorem simprr2 1222

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 1137	. 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:  poxp2  8169  icodiamlt  15475  psgnunilem2  19514  haust1  23361  cnhaus  23363  isreg2  23386  llynlly  23486  restnlly  23491  llyrest  23494  llyidm  23497  nllyidm  23498  cldllycmp  23504  txlly  23645  txnlly  23646  pthaus  23647  txhaus  23656  txkgen  23661  xkohaus  23662  xkococnlem  23668  cmetcaulem  25323  itg2add  25795  ulmdvlem3  26446  nosupprefixmo  27746  noinfprefixmo  27747  etasslt  27859  scutbdaybnd  27861  scutbdaybnd2  27862  addsproplem6  28008  negsproplem6  28066  mulsproplem13  28155  mulsproplem14  28156  mulsprop  28157  ax5seglem6  28950  n4cyclfrgr  30311  connpconn  35241  cvmlift3lem2  35326  cvmlift3lem8  35332  broutsideof3  36128  unblimceq0  36509  paddasslem10  39832  lhpexle2lem  40012  lhpexle3lem  40014  stoweidlem35  46055  stoweidlem56  46076  stoweidlem59  46079