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

Theorem ancrd 561
Description: Deduction conjoining antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.)
Hypothesis
Ref Expression
ancrd.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
ancrd  |-  ( ph  ->  ( ps  ->  ( ch  /\  ps ) ) )

Proof of Theorem ancrd
StepHypRef Expression
1 ancrd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 idd 25 . 2  |-  ( ph  ->  ( ps  ->  ps ) )
31, 2jcad 540 1  |-  ( ph  ->  ( ps  ->  ( ch  /\  ps ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  impac  631  equviniv  1883  reupick  3739  prel12  4165  reusv2lem3  4623  ssrnres  5297  funmo  5621  funssres  5645  dffo4  6066  dffo5  6067  dfwe2  6640  ordpwsuc  6674  ordunisuc2  6703  dfom2  6726  nnsuc  6741  nnaordex  7370  wdom2d  8126  iundom2g  8996  fzospliti  11987  rexuz3  13466  prmdvdsfz  14704  qredeq  14718  dirge  16538  lssssr  18231  lpigen  18535  psgnodpm  19211  neiptopnei  20203  metustexhalf  21626  dyadmbllem  22613  3cyclfrgrarn2  25798  atexch  28090  ordtconlem1  28781  isbasisrelowllem1  31804  isbasisrelowllem2  31805  phpreu  31975  poimirlem26  32012  sstotbnd3  32154  eqlkr3  32713  dihatexv  34952  dvh3dim2  35062  pm14.123b  36822  ordpss  36849  climreeq  37779  reuan  38736  2reu1  38742  ssrelrn  39148
  Copyright terms: Public domain W3C validator