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

Theorem simp1rr 1240
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp1rr (((𝜒 ∧ (𝜑𝜓)) ∧ 𝜃𝜏) → 𝜓)

Proof of Theorem simp1rr
StepHypRef Expression
1 simprr 773 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜓)
213ad2ant1 1134 1 (((𝜒 ∧ (𝜑𝜓)) ∧ 𝜃𝜏) → 𝜓)
Colors of variables: wff setvar class
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:  f1imass  7284  smo11  8404  zsupss  12979  lsmcv  21143  lspsolvlem  21144  mat2pmatghm  22736  mat2pmatmul  22737  nrmr0reg  23757  plyadd  26256  plymul  26257  coeeu  26264  ax5seglem6  28949  archiabl  33205  mdetpmtr1  33822  sseqval  34390  wsuclem  35826  btwnconn1lem1  36088  btwnconn1lem2  36089  btwnconn1lem12  36099  lshpsmreu  39110  1cvratlt  39476  llnle  39520  lvolex3N  39540  lnjatN  39782  lncvrat  39784  lncmp  39785  cdlemd6  40205  cdlemk19ylem  40932  pellex  42846  tfsconcatrn  43355  limcperiod  45643  itschlc0xyqsol1  48687  itschlc0xyqsol  48688
  Copyright terms: Public domain W3C validator