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

Theorem anim1d 548
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 22 . 2  |-  ( ph  ->  ( th  ->  th )
)
31, 2anim12d 547 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  pm3.45  808  ax12olem2OLD  2012  exdistrf  2062  exdistrfOLD  2063  mopick2  2347  ssrexv  3400  ssdif  3474  ssrin  3558  reupick  3617  disjss1  4180  copsexg  4434  po3nr  4509  frss  4541  ordsssuc2  4662  coss2  5021  fununi  5509  dffv2  5788  onfununi  6595  oaass  6796  ssnnfi  7320  fiint  7375  fiss  7421  wemapso2lem  7511  cantnfreslem  7623  tcss  7675  ac6s  8356  reclem2pr  8917  qbtwnxr  10778  ico0  10954  icoshft  11011  r19.2uz  12147  infpn2  13273  fthres2  14121  ablfacrplem  15615  neiss  17165  uptx  17649  txcn  17650  nrmr0reg  17773  cnpflfi  18023  cnextcn  18090  caussi  19242  ovolsslem  19372  cycliscrct  21609  shorth  22789  poseq  25520  nodenselem5  25632  trisegint  25954  segcon2  26031  itg2addnclem  26246  itg2addnclem2  26247  opnrebl2  26315  fdc1  26441  totbndss  26477  ablo4pnp  26546  keridl  26633  pell14qrss1234  26910  pell1qrss14  26922  rmxycomplete  26971  lnr2i  27288  ssrexf  27651  rfcnnnub  27674  ax12olem2wAUX7  29393  exdistrfNEW7  29442  ax12olem2OLD7  29643  dib2dim  31978  dih2dimbALTN  31980  dvh1dim  32177  mapdpglem2  32408
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 178  df-an 361
  Copyright terms: Public domain W3C validator