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

Theorem ancri 537
Description: Deduction conjoining antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.)
Hypothesis
Ref Expression
ancri.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ancri  |-  ( ph  ->  ( ps  /\  ph ) )

Proof of Theorem ancri
StepHypRef Expression
1 ancri.1 . 2  |-  ( ph  ->  ps )
2 id 21 . 2  |-  ( ph  ->  ph )
31, 2jca 520 1  |-  ( ph  ->  ( ps  /\  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  truan  1341  bamalip  2403  gencbvex  3000  trsuc  4669  eusv2nf  4724  issref  5250  fo00  5714  eqfnov2  6180  caovmo  6287  bropopvvv  6429  tz7.48lem  6701  tz7.48-1  6703  oewordri  6838  epfrs  7670  ordpipq  8824  ltexprlem4  8921  xrinfmsslem  10891  catpropd  13940  icccvx  18980  0wlkon  21552  esumcst  24460  dfpo2  25383  iotasbc  27610  wallispilem3  27806  hash2prv  28193  swrdccat3a  28251  cshweqdifid  28306  2wlkonot3v  28407  2spthonot3v  28408  bnj600  29364  bnj852  29366
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 179  df-an 362
  Copyright terms: Public domain W3C validator