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

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

Proof of Theorem simp1rl
StepHypRef Expression
1 simprl 793 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜑)
213ad2ant1 1080 1 (((𝜒 ∧ (𝜑𝜓)) ∧ 𝜃𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  f1imass  6476  smo11  7407  zsupss  11721  lsmcv  19055  lspsolvlem  19056  mat2pmatghm  20449  mat2pmatmul  20450  plyadd  23872  plymul  23873  coeeu  23880  aannenlem1  23982  logexprlim  24845  ax5seglem6  25709  ax5seg  25713  mdetpmtr1  29663  mdetpmtr2  29664  wsuclem  31466  wsuclemOLD  31467  btwnconn1lem2  31829  btwnconn1lem3  31830  btwnconn1lem4  31831  btwnconn1lem12  31839  lshpsmreu  33862  2llnmat  34276  lvolex3N  34290  lnjatN  34532  pclfinclN  34702  lhpat3  34798  cdlemd6  34956  cdlemfnid  35318  cdlemk19ylem  35684  dihlsscpre  35989  dih1dimb2  35996  dihglblem6  36095  pellex  36865  mullimc  39239  mullimcf  39246  limcperiod  39251  cncfshift  39377  cncfperiod  39382
  Copyright terms: Public domain W3C validator