MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anim1d 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  1966  exdistrf  2010  mopick2  2305  ssrexv  3351  ssdif  3425  ssrin  3509  reupick  3568  disjss1  4129  copsexg  4383  po3nr  4458  frss  4490  ordsssuc2  4610  coss2  4969  fununi  5457  dffv2  5735  onfununi  6539  oaass  6740  ssnnfi  7264  fiint  7319  fiss  7364  wemapso2lem  7452  cantnfreslem  7564  tcss  7616  ac6s  8297  reclem2pr  8858  qbtwnxr  10718  ico0  10894  icoshft  10951  r19.2uz  12082  infpn2  13208  fthres2  14056  ablfacrplem  15550  neiss  17096  uptx  17578  txcn  17579  nrmr0reg  17702  cnpflfi  17952  cnextcn  18019  caussi  19121  ovolsslem  19247  cycliscrct  21465  shorth  22645  poseq  25277  nodenselem5  25363  trisegint  25676  segcon2  25753  itg2addnclem  25957  itg2addnclem2  25958  opnrebl2  26015  fdc1  26141  totbndss  26177  ablo4pnp  26246  keridl  26333  pell14qrss1234  26610  pell1qrss14  26622  rmxycomplete  26671  lnr2i  26989  ssrexf  27352  rfcnnnub  27375  ax12olem2wAUX7  28794  exdistrfNEW7  28843  ax12olem2OLD7  29022  dib2dim  31358  dih2dimbALTN  31360  dvh1dim  31557  mapdpglem2  31788
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