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

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

Proof of Theorem simp1rr
StepHypRef Expression
1 simprr 771 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜓)
213ad2ant1 1129 1 (((𝜒 ∧ (𝜑𝜓)) ∧ 𝜃𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  w3a 1083
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 209  df-an 399  df-3an 1085
This theorem is referenced by:  f1imass  7016  smo11  7995  zsupss  12331  lsmcv  19907  lspsolvlem  19908  mat2pmatghm  21332  mat2pmatmul  21333  nrmr0reg  22351  plyadd  24801  plymul  24802  coeeu  24809  ax5seglem6  26714  archiabl  30822  mdetpmtr1  31083  sseqval  31641  wsuclem  33107  btwnconn1lem1  33543  btwnconn1lem2  33544  btwnconn1lem12  33554  lshpsmreu  36239  1cvratlt  36604  llnle  36648  lvolex3N  36668  lnjatN  36910  lncvrat  36912  lncmp  36913  cdlemd6  37333  cdlemk19ylem  38060  pellex  39425  limcperiod  41902  itschlc0xyqsol1  44747  itschlc0xyqsol  44748
  Copyright terms: Public domain W3C validator