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

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

Proof of Theorem simp1rl
StepHypRef Expression
1 simprl 770 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜑)
213ad2ant1 1130 1 (((𝜒 ∧ (𝜑𝜓)) ∧ 𝜃𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  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 210  df-an 400  df-3an 1086
This theorem is referenced by:  f1imass  7004  smo11  7988  zsupss  12329  lsmcv  19909  lspsolvlem  19910  mat2pmatghm  21338  mat2pmatmul  21339  plyadd  24817  plymul  24818  coeeu  24825  aannenlem1  24927  logexprlim  25812  ax5seglem6  26731  ax5seg  26735  mdetpmtr1  31176  mdetpmtr2  31177  wsuclem  33220  btwnconn1lem2  33657  btwnconn1lem3  33658  btwnconn1lem4  33659  btwnconn1lem12  33667  lshpsmreu  36398  2llnmat  36813  lvolex3N  36827  lnjatN  37069  pclfinclN  37239  lhpat3  37335  cdlemd6  37492  cdlemfnid  37853  cdlemk19ylem  38219  dihlsscpre  38523  dih1dimb2  38530  dihglblem6  38629  pellex  39763  mullimc  42245  mullimcf  42252  limcperiod  42257  cncfshift  42503  cncfperiod  42508
  Copyright terms: Public domain W3C validator