Theorem simprr2 1223

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  8083  icodiamlt  15363  psgnunilem2  19392  haust1  23255  cnhaus  23257  isreg2  23280  llynlly  23380  restnlly  23385  llyrest  23388  llyidm  23391  nllyidm  23392  cldllycmp  23398  txlly  23539  txnlly  23540  pthaus  23541  txhaus  23550  txkgen  23555  xkohaus  23556  xkococnlem  23562  cmetcaulem  25204  itg2add  25676  ulmdvlem3  26327  nosupprefixmo  27628  noinfprefixmo  27629  etasslt  27742  scutbdaybnd  27744  scutbdaybnd2  27745  addsproplem6  27904  negsproplem6  27962  mulsproplem13  28054  mulsproplem14  28055  mulsprop  28056  ax5seglem6  28897  n4cyclfrgr  30253  connpconn  35207  cvmlift3lem2  35292  cvmlift3lem8  35298  broutsideof3  36099  unblimceq0  36480  paddasslem10  39808  lhpexle2lem  39988  lhpexle3lem  39990  stoweidlem35  46017  stoweidlem56  46038  stoweidlem59  46041  pgn4cyclex  48100  2arwcat  49573