MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simprr2 Structured version   Visualization version   GIF version

Theorem simprr2 1219
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
StepHypRef Expression
1 simp2 1134 . 2 ((𝜑𝜓𝜒) → 𝜓)
21ad2antll 726 1 ((𝜏 ∧ (𝜃 ∧ (𝜑𝜓𝜒))) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1084
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 206  df-an 396  df-3an 1086
This theorem is referenced by:  poxp2  8123  icodiamlt  15379  psgnunilem2  19405  haust1  23178  cnhaus  23180  isreg2  23203  llynlly  23303  restnlly  23308  llyrest  23311  llyidm  23314  nllyidm  23315  cldllycmp  23321  txlly  23462  txnlly  23463  pthaus  23464  txhaus  23473  txkgen  23478  xkohaus  23479  xkococnlem  23485  cmetcaulem  25138  itg2add  25611  ulmdvlem3  26255  nosupprefixmo  27549  noinfprefixmo  27550  etasslt  27662  scutbdaybnd  27664  scutbdaybnd2  27665  addsproplem6  27807  negsproplem6  27861  mulsproplem13  27944  mulsproplem14  27945  mulsprop  27946  ax5seglem6  28661  n4cyclfrgr  30013  connpconn  34715  cvmlift3lem2  34800  cvmlift3lem8  34806  broutsideof3  35593  unblimceq0  35873  paddasslem10  39190  lhpexle2lem  39370  lhpexle3lem  39372  stoweidlem35  45236  stoweidlem56  45257  stoweidlem59  45260
  Copyright terms: Public domain W3C validator