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

Theorem anim2d 605
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 602 1 (𝜑 → ((𝜃𝜓) → (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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
This theorem is referenced by:  sbimd  2275  darii  2688  festino  2699  baroco  2701  moeq3  3544  ssel  3757  sscon  3908  uniss  4619  trel3  4921  ssopab2  5164  coss1  5448  fununi  6144  imadif  6153  fss  6238  ssimaex  6454  ssoprab2  6911  poxp  7493  soxp  7494  pmss12g  8089  ss2ixp  8128  xpdom2  8264  fisup2g  8583  fisupcl  8584  fiinf2g  8615  inf3lem1  8742  epfrs  8824  cfub  9326  cflm  9327  fin23lem34  9423  isf32lem2  9431  axcc4  9516  domtriomlem  9519  ltexprlem3  10115  nnunb  11536  indstr  11960  qbtwnxr  12236  qsqueeze  12237  xrsupsslem  12342  xrinfmsslem  12343  ioc0  12427  climshftlem  14593  o1rlimmul  14637  ramub2  16000  monmat2matmon  20911  tgcl  21056  neips  21200  ssnei2  21203  tgcnp  21340  cnpnei  21351  cnpco  21354  hauscmplem  21492  hauscmp  21493  llyss  21565  nllyss  21566  lfinun  21611  kgen2ss  21641  txcnpi  21694  txcmplem1  21727  fgss  21959  cnpflf2  22086  fclsss1  22108  fclscf  22111  alexsubALT  22137  cnextcn  22153  tsmsxp  22240  mopni3  22581  psmetutop  22654  tngngp3  22742  iscau4  23359  caussi  23377  ovolgelb  23541  mbfi1flim  23784  ellimc3  23937  lhop1  24071  tgbtwndiff  25695  axcontlem4  26141  sspmval  28047  shmodsi  28707  atcvat4i  29715  cdj3lem2b  29755  ifeqeqx  29813  acunirnmpt  29912  xrge0infss  29977  crefss  30366  issgon  30636  cvmlift2lem12  31747  ss2mcls  31916  poseq  32200  btwndiff  32581  seglecgr12im  32664  fnessref  32798  waj-ax  32855  lukshef-ax2  32856  icorempt2  33635  finxpreclem1  33662  tan2h  33828  poimirlem31  33867  poimir  33869  mblfinlem3  33875  mblfinlem4  33876  ismblfin  33877  cvrat4  35402  athgt  35415  ps-2  35437  paddss1  35776  paddss2  35777  cdlemg33b0  36660  cdlemg33a  36665  dihjat1lem  37387  fphpdo  38062  irrapxlem2  38068  pell14qrss1234  38101  pell1qrss14  38113  acongtr  38225  ax6e2eq  39438  islptre  40492  limccog  40493
  Copyright terms: Public domain W3C validator