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

Theorem anim1d 612
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 610 1 (𝜑 → ((𝜓𝜃) → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398
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 209  df-an 399
This theorem is referenced by:  pm3.45  623  exdistrf  2462  2ax6elem  2486  mopick2  2716  ssrexf  4029  ssrexv  4032  ssdif  4114  ssrin  4208  reupick  4285  disjss1  5028  copsexgw  5372  copsexg  5373  propeqop  5388  po3nr  5481  frss  5515  coss2  5720  ordsssuc2  6272  fununi  6422  dffv2  6749  oprabidw  7179  extmptsuppeq  7846  onfununi  7970  oaass  8179  ssnnfi  8729  fiint  8787  fiss  8880  wemapsolem  9006  tcss  9178  ac6s  9898  reclem2pr  10462  qbtwnxr  12585  ico0  12776  icoshft  12851  2ffzeq  13020  clsslem  14336  r19.2uz  14703  isprm7  16044  infpn2  16241  prmgaplem4  16382  fthres2  17194  ablfacrplem  19179  monmat2matmon  21424  neiss  21709  uptx  22225  txcn  22226  nrmr0reg  22349  cnpflfi  22599  cnextcn  22667  caussi  23892  ovolsslem  24077  tgtrisegint  26277  inagswap  26619  shorth  29064  mptssALT  30412  uzssico  30499  ordtconnlem1  31155  omsmon  31544  omssubadd  31546  subgrtrl  32368  subgrcycl  32370  acycgrsubgr  32393  mclsax  32804  poseq  33083  trisegint  33477  segcon2  33554  opnrebl2  33657  bj-19.42t  34090  poimirlem30  34909  itg2addnclem  34930  itg2addnclem2  34931  fdc1  35008  totbndss  35042  ablo4pnp  35145  keridl  35297  dib2dim  38366  dih2dimbALTN  38368  dvh1dim  38565  mapdpglem2  38796  pell14qrss1234  39438  pell1qrss14  39450  rmxycomplete  39499  lnr2i  39701  rp-fakeanorass  39864  rfcnnnub  41278  or2expropbi  43254  2ffzoeq  43513  ich2exprop  43618  nnsum4primes4  43939  nnsum4primesprm  43941  nnsum4primesgbe  43943  nnsum4primesle9  43945
  Copyright terms: Public domain W3C validator