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

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

Proof of Theorem simp1rl
StepHypRef Expression
1 simprl 787 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜑)
213ad2ant1 1163 1 (((𝜒 ∧ (𝜑𝜓)) ∧ 𝜃𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107
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 198  df-an 385  df-3an 1109
This theorem is referenced by:  f1imass  6713  smo11  7665  zsupss  11978  lsmcv  19414  lspsolvlem  19415  mat2pmatghm  20814  mat2pmatmul  20815  plyadd  24264  plymul  24265  coeeu  24272  aannenlem1  24374  logexprlim  25241  ax5seglem6  26105  ax5seg  26109  mdetpmtr1  30271  mdetpmtr2  30272  wsuclem  32146  btwnconn1lem2  32571  btwnconn1lem3  32572  btwnconn1lem4  32573  btwnconn1lem12  32581  lshpsmreu  34997  2llnmat  35412  lvolex3N  35426  lnjatN  35668  pclfinclN  35838  lhpat3  35934  cdlemd6  36091  cdlemfnid  36452  cdlemk19ylem  36818  dihlsscpre  37122  dih1dimb2  37129  dihglblem6  37228  pellex  38009  mullimc  40418  mullimcf  40425  limcperiod  40430  cncfshift  40657  cncfperiod  40662
  Copyright terms: Public domain W3C validator