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

Theorem anim2d 587
Description: Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 14-May-1993.)
Hypothesis
Ref Expression
anim1d.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
anim2d (𝜑 → ((𝜃𝜓) → (𝜃𝜒)))

Proof of Theorem anim2d
StepHypRef Expression
1 idd 24 . 2 (𝜑 → (𝜃𝜃))
2 anim1d.1 . 2 (𝜑 → (𝜓𝜒))
31, 2anim12d 584 1 (𝜑 → ((𝜃𝜓) → (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 196  df-an 385
This theorem is referenced by:  eleq2dOLD  2674  moeq3  3350  ssel  3562  sscon  3706  uniss  4394  trel3  4688  ssopab2  4926  coss1  5199  fununi  5878  imadif  5887  fss  5969  ssimaex  6173  ssoprab2  6609  poxp  7176  soxp  7177  pmss12g  7770  ss2ixp  7807  xpdom2  7940  fisup2g  8257  fisupcl  8258  fiinf2g  8289  inf3lem1  8408  epfrs  8490  cfub  8954  cflm  8955  fin23lem34  9051  isf32lem2  9059  axcc4  9144  domtriomlem  9147  ltexprlem3  9739  nnunb  11165  indstr  11632  qbtwnxr  11905  qsqueeze  11906  xrsupsslem  12009  xrinfmsslem  12010  ioc0  12093  climshftlem  14153  o1rlimmul  14197  ramub2  15556  monmat2matmon  20448  tgcl  20584  neips  20727  ssnei2  20730  tgcnp  20867  cnpnei  20878  cnpco  20881  hauscmplem  21019  hauscmp  21020  llyss  21092  nllyss  21093  lfinun  21138  kgen2ss  21168  txcnpi  21221  txcmplem1  21254  fgss  21487  cnpflf2  21614  fclsss1  21636  fclscf  21639  alexsubALT  21665  cnextcn  21681  tsmsxp  21768  mopni3  22109  psmetutop  22182  tngngp3  22270  iscau4  22885  caussi  22903  ovolgelb  23055  mbfi1flim  23296  ellimc3  23449  lhop1  23581  tgbtwndiff  25201  axcontlem4  25647  iswlkg  26052  sspmval  26972  shmodsi  27632  atcvat4i  28640  cdj3lem2b  28680  ifeqeqx  28745  acunirnmpt  28841  xrge0infss  28915  crefss  29244  issgon  29513  cvmlift2lem12  30550  ss2mcls  30719  poseq  30994  btwndiff  31304  seglecgr12im  31387  fnessref  31522  waj-ax  31583  lukshef-ax2  31584  icorempt2  32375  finxpreclem1  32402  tan2h  32571  poimirlem31  32610  poimir  32612  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  cvrat4  33747  athgt  33760  ps-2  33782  paddss1  34121  paddss2  34122  cdlemg33b0  35007  cdlemg33a  35012  dihjat1lem  35735  fphpdo  36399  irrapxlem2  36405  pell14qrss1234  36438  pell1qrss14  36450  acongtr  36563  ax6e2eq  37794  islptre  38686  limccog  38687
  Copyright terms: Public domain W3C validator