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

Theorem anim2d 614
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 611 1 (𝜑 → ((𝜃𝜓) → (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  darii  2727  festino  2736  baroco  2738  moeq3  3651  ssel  3908  sselOLD  3909  sscon  4066  uniss  4808  trel3  5144  ssopab2  5398  coss1  5690  fununi  6399  imadif  6408  fss  6501  ssimaex  6723  ssoprab2  7201  poxp  7805  soxp  7806  suppofssd  7850  pmss12g  8416  ss2ixp  8457  xpdom2  8595  fisup2g  8916  fisupcl  8917  fiinf2g  8948  inf3lem1  9075  epfrs  9157  cfub  9660  cflm  9661  fin23lem34  9757  isf32lem2  9765  axcc4  9850  domtriomlem  9853  ltexprlem3  10449  nnunb  11881  indstr  12304  qbtwnxr  12581  qsqueeze  12582  xrsupsslem  12688  xrinfmsslem  12689  ioc0  12773  climshftlem  14923  o1rlimmul  14967  ramub2  16340  monmat2matmon  21429  tgcl  21574  neips  21718  ssnei2  21721  tgcnp  21858  cnpnei  21869  cnpco  21872  hauscmplem  22011  hauscmp  22012  llyss  22084  nllyss  22085  lfinun  22130  kgen2ss  22160  txcnpi  22213  txcmplem1  22246  fgss  22478  cnpflf2  22605  fclsss1  22627  fclscf  22630  alexsubALT  22656  cnextcn  22672  tsmsxp  22760  mopni3  23101  psmetutop  23174  tngngp3  23262  iscau4  23883  caussi  23901  ovolgelb  24084  mbfi1flim  24327  ellimc3  24482  lhop1  24617  tgbtwndiff  26300  axcontlem4  26761  clwwlknonwwlknonb  27891  sspmval  28516  shmodsi  29172  atcvat4i  30180  cdj3lem2b  30220  ifeqeqx  30309  acunirnmpt  30422  xrge0infss  30510  crefss  31202  issgon  31492  cvmlift2lem12  32674  satfv1  32723  satfvsucsuc  32725  ss2mcls  32928  poseq  33208  btwndiff  33601  seglecgr12im  33684  fnessref  33818  waj-ax  33875  lukshef-ax2  33876  icorempo  34768  finxpreclem1  34806  fvineqsneq  34829  pibt2  34834  tan2h  35049  poimirlem31  35088  poimir  35090  mblfinlem3  35096  mblfinlem4  35097  ismblfin  35098  cvrat4  36739  athgt  36752  ps-2  36774  paddss1  37113  paddss2  37114  cdlemg33b0  37997  cdlemg33a  38002  dihjat1lem  38724  fphpdo  39756  irrapxlem2  39762  pell14qrss1234  39795  pell1qrss14  39807  acongtr  39917  grumnudlem  40991  ax6e2eq  41261  islptre  42259  limccog  42260
  Copyright terms: Public domain W3C validator