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  1869  exdistrf  1911  mopick2  2210  ssrexv  3238  ssdif  3311  ssrin  3394  reupick  3452  disjss1  3999  copsexg  4252  po3nr  4328  frss  4360  ordsssuc2  4481  coss2  4840  fununi  5316  dffv2  5592  onfununi  6358  oaass  6559  ssnnfi  7082  fiint  7133  fiss  7177  wemapso2lem  7265  cantnfreslem  7377  tcss  7429  ac6s  8111  reclem2pr  8672  qbtwnxr  10527  ico0  10702  icoshft  10758  r19.2uz  11835  infpn2  12960  fthres2  13806  ablfacrplem  15300  neiss  16846  uptx  17319  txcn  17320  nrmr0reg  17440  cnpflfi  17694  caussi  18723  ovolsslem  18843  shorth  21874  poseq  24253  nodenselem5  24339  trisegint  24651  segcon2  24728  untim1d  25020  oprabex2gpop  25036  opnrebl2  26236  fdc1  26456  totbndss  26501  ablo4pnp  26570  keridl  26657  pell14qrss1234  26941  pell1qrss14  26953  rmxycomplete  27002  lnr2i  27320  ssrexf  27684  dib2dim  31433  dih2dimbALTN  31435  dvh1dim  31632  mapdpglem2  31863
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