Theorem simprr2 1224

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  poxp2  8093  icodiamlt  15400  psgnunilem2  19470  haust1  23317  cnhaus  23319  isreg2  23342  llynlly  23442  restnlly  23447  llyrest  23450  llyidm  23453  nllyidm  23454  cldllycmp  23460  txlly  23601  txnlly  23602  pthaus  23603  txhaus  23612  txkgen  23617  xkohaus  23618  xkococnlem  23624  cmetcaulem  25255  itg2add  25726  ulmdvlem3  26367  nosupprefixmo  27664  noinfprefixmo  27665  etaslts  27785  cutbdaybnd  27787  cutbdaybnd2  27788  addsproplem6  27966  negsproplem6  28025  mulsproplem13  28120  mulsproplem14  28121  mulsprop  28122  bdayfinbndlem1  28459  ax5seglem6  29003  n4cyclfrgr  30361  connpconn  35417  cvmlift3lem2  35502  cvmlift3lem8  35508  broutsideof3  36308  unblimceq0  36767  paddasslem10  40275  lhpexle2lem  40455  lhpexle3lem  40457  stoweidlem35  46463  stoweidlem56  46484  stoweidlem59  46487  pgn4cyclex  48602  2arwcat  50075