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

Theorem anim1d 586
Description: Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.)
Hypothesis
Ref Expression
anim1d.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
anim1d (𝜑 → ((𝜓𝜃) → (𝜒𝜃)))

Proof of Theorem anim1d
StepHypRef Expression
1 anim1d.1 . 2 (𝜑 → (𝜓𝜒))
2 idd 24 . 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:  pm3.45  875  exdistrf  2321  2ax6elem  2437  mopick2  2528  ssrexf  3628  ssrexv  3630  ssdif  3707  ssrin  3800  reupick  3870  disjss1  4559  copsexg  4882  propeqop  4895  po3nr  4973  frss  5005  coss2  5200  ordsssuc2  5731  fununi  5878  dffv2  6181  extmptsuppeq  7206  onfununi  7325  oaass  7528  ssnnfi  8064  fiint  8122  fiss  8213  wemapsolem  8338  tcss  8503  ac6s  9189  reclem2pr  9749  qbtwnxr  11905  ico0  12092  icoshft  12165  2ffzeq  12329  clsslem  13571  r19.2uz  13939  isprm7  15258  infpn2  15455  prmgaplem4  15596  fthres2  16415  ablfacrplem  18287  monmat2matmon  20448  neiss  20723  uptx  21238  txcn  21239  nrmr0reg  21362  cnpflfi  21613  cnextcn  21681  caussi  22903  ovolsslem  23059  tgtrisegint  25194  inagswap  25530  cycliscrct  26158  numclwwlkovgelim  26616  shorth  27538  mptssALT  28857  ordtconlem1  29298  omsmon  29687  omssubadd  29689  mclsax  30720  poseq  30994  nodenselem5  31084  trisegint  31305  segcon2  31382  opnrebl2  31486  poimirlem30  32609  itg2addnclem  32631  itg2addnclem2  32632  fdc1  32712  totbndss  32746  ablo4pnp  32849  keridl  33001  dib2dim  35550  dih2dimbALTN  35552  dvh1dim  35749  mapdpglem2  35980  pell14qrss1234  36438  pell1qrss14  36450  rmxycomplete  36500  lnr2i  36705  rp-fakeanorass  36877  rfcnnnub  38218  nnsum4primes4  40205  nnsum4primesprm  40207  nnsum4primesgbe  40209  nnsum4primesle9  40211  2ffzoeq  40361  cyclisCrct  41005  clwwlknp  41195
  Copyright terms: Public domain W3C validator