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

Theorem anim1d 547
Description: Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.)
Hypothesis
Ref Expression
anim1d.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
anim1d  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
th ) ) )

Proof of Theorem anim1d
StepHypRef Expression
1 anim1d.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 idd 21 . 2  |-  ( ph  ->  ( th  ->  th )
)
31, 2anim12d 546 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  pm3.45  807  ax12olem2  1881  exdistrf  1924  mopick2  2223  ssrexv  3251  ssdif  3324  ssrin  3407  reupick  3465  disjss1  4015  copsexg  4268  po3nr  4344  frss  4376  ordsssuc2  4497  coss2  4856  fununi  5332  dffv2  5608  onfununi  6374  oaass  6575  ssnnfi  7098  fiint  7149  fiss  7193  wemapso2lem  7281  cantnfreslem  7393  tcss  7445  ac6s  8127  reclem2pr  8688  qbtwnxr  10543  ico0  10718  icoshft  10774  r19.2uz  11851  infpn2  12976  fthres2  13822  ablfacrplem  15316  neiss  16862  uptx  17335  txcn  17336  nrmr0reg  17456  cnpflfi  17710  caussi  18739  ovolsslem  18859  shorth  21890  poseq  24324  nodenselem5  24410  trisegint  24723  segcon2  24800  itg2addnclem  25003  itg2addnclem2  25004  untim1d  25123  oprabex2gpop  25139  opnrebl2  26339  fdc1  26559  totbndss  26604  ablo4pnp  26673  keridl  26760  pell14qrss1234  27044  pell1qrss14  27056  rmxycomplete  27105  lnr2i  27423  ssrexf  27787  cycliscrct  28375  ax12olem2wAUX7  29433  exdistrfNEW7  29482  ax12olem2OLD7  29660  dib2dim  32055  dih2dimbALTN  32057  dvh1dim  32254  mapdpglem2  32485
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator