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 728	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  8184  icodiamlt  15484  psgnunilem2  19537  haust1  23381  cnhaus  23383  isreg2  23406  llynlly  23506  restnlly  23511  llyrest  23514  llyidm  23517  nllyidm  23518  cldllycmp  23524  txlly  23665  txnlly  23666  pthaus  23667  txhaus  23676  txkgen  23681  xkohaus  23682  xkococnlem  23688  cmetcaulem  25341  itg2add  25814  ulmdvlem3  26463  nosupprefixmo  27763  noinfprefixmo  27764  etasslt  27876  scutbdaybnd  27878  scutbdaybnd2  27879  addsproplem6  28025  negsproplem6  28083  mulsproplem13  28172  mulsproplem14  28173  mulsprop  28174  ax5seglem6  28967  n4cyclfrgr  30323  connpconn  35203  cvmlift3lem2  35288  cvmlift3lem8  35294  broutsideof3  36090  unblimceq0  36473  paddasslem10  39786  lhpexle2lem  39966  lhpexle3lem  39968  stoweidlem35  45956  stoweidlem56  45977  stoweidlem59  45980