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

Theorem anim1d 566
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 25 . 2  |-  ( ph  ->  ( th  ->  th )
)
31, 2anim12d 565 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  pm3.45  842  exdistrf  2131  2ax6elem  2245  mopick2  2340  ssrexf  3530  ssrexv  3532  ssdif  3606  ssrin  3693  reupick  3763  disjss1  4403  copsexg  4707  po3nr  4789  frss  4821  coss2  5011  ordsssuc2  5530  fununi  5667  dffv2  5954  extmptsuppeq  6950  onfununi  7068  oaass  7270  ssnnfi  7797  fiint  7854  fiss  7944  wemapsolem  8065  tcss  8227  ac6s  8912  reclem2pr  9472  qbtwnxr  11493  ico0  11682  icoshft  11752  2ffzeq  11908  clsslem  13027  r19.2uz  13393  infpn2  14820  prmgaplem4  14987  fthres2  15788  ablfacrplem  17633  monmat2matmon  19779  neiss  20056  uptx  20571  txcn  20572  nrmr0reg  20695  cnpflfi  20945  cnextcn  21013  caussi  22160  ovolsslem  22315  tgtrisegint  24406  inagswap  24733  cycliscrct  25203  numclwwlkovgelim  25662  shorth  26783  fmptss  28117  ordtconlem1  28569  omsmon  28959  omssubadd  28961  mclsax  29995  poseq  30278  nodenselem5  30359  trisegint  30580  segcon2  30657  opnrebl2  30762  poimirlem30  31674  itg2addnclem  31697  itg2addnclem2  31698  fdc1  31779  totbndss  31813  ablo4pnp  31882  keridl  31969  dib2dim  34520  dih2dimbALTN  34522  dvh1dim  34719  mapdpglem2  34950  pell14qrss1234  35410  pell1qrss14  35422  rmxycomplete  35471  lnr2i  35681  rp-fakeanorass  35856  isprm7  36297  rfcnnnub  36997  nnsum4primes4  38274  nnsum4primesprm  38276  nnsum4primesgbe  38278  nnsum4primesle9  38280  2ffzoeq  38413
  Copyright terms: Public domain W3C validator