Theorem simprr2 1241

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 1155	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antll 741	1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  poxp2  8140  icodiamlt  15491  psgnunilem2  19566  haust1  23490  cnhaus  23492  isreg2  23515  llynlly  23615  restnlly  23620  llyrest  23623  llyidm  23626  nllyidm  23627  cldllycmp  23633  txlly  23774  txnlly  23775  pthaus  23776  txhaus  23785  txkgen  23790  xkohaus  23791  xkococnlem  23797  cmetcaulem  25428  itg2add  25899  ulmdvlem3  26543  nosupprefixmo  27842  noinfprefixmo  27843  etaslts  27964  cutbdaybnd  27966  cutbdaybnd2  27967  addsproplem6  28145  negsproplem6  28204  mulsproplem13  28299  mulsproplem14  28300  mulsprop  28301  bdayfinbndlem1  28638  ax5seglem6  29262  n4cyclfrgr  30620  connpconn  35705  cvmlift3lem2  35790  cvmlift3lem8  35796  broutsideof3  36596  unblimceq0  37074  paddasslem10  40581  lhpexle2lem  40761  lhpexle3lem  40763  stoweidlem35  46729  stoweidlem56  46750  stoweidlem59  46753  pgn4cyclex  48868  2arwcat  50355