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

Theorem anim1d 589
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 587 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 197  df-an 385
This theorem is referenced by:  pm3.45  915  exdistrf  2474  2ax6elem  2587  mopick2  2679  ssrexf  3807  ssrexv  3809  ssdif  3889  ssrin  3982  reupick  4055  disjss1  4779  copsexg  5105  propeqop  5119  po3nr  5202  frss  5234  coss2  5435  ordsssuc2  5976  fununi  6126  dffv2  6435  extmptsuppeq  7489  onfununi  7609  oaass  7813  ssnnfi  8347  fiint  8405  fiss  8498  wemapsolem  8623  tcss  8796  ac6s  9519  reclem2pr  10083  qbtwnxr  12245  ico0  12435  icoshft  12508  2ffzeq  12675  clsslem  13945  r19.2uz  14311  isprm7  15643  infpn2  15840  prmgaplem4  15981  fthres2  16814  ablfacrplem  18685  monmat2matmon  20852  neiss  21136  uptx  21651  txcn  21652  nrmr0reg  21775  cnpflfi  22025  cnextcn  22093  caussi  23316  ovolsslem  23473  tgtrisegint  25615  inagswap  25951  shorth  28485  mptssALT  29805  uzssico  29877  ordtconnlem1  30301  omsmon  30691  omssubadd  30693  mclsax  31795  poseq  32081  trisegint  32463  segcon2  32540  opnrebl2  32644  poimirlem30  33771  itg2addnclem  33793  itg2addnclem2  33794  fdc1  33874  totbndss  33908  ablo4pnp  34011  keridl  34163  dib2dim  37053  dih2dimbALTN  37055  dvh1dim  37252  mapdpglem2  37483  pell14qrss1234  37941  pell1qrss14  37953  rmxycomplete  38003  lnr2i  38207  rp-fakeanorass  38379  rfcnnnub  39713  2ffzoeq  41867  nnsum4primes4  42206  nnsum4primesprm  42208  nnsum4primesgbe  42210  nnsum4primesle9  42212
  Copyright terms: Public domain W3C validator