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

Theorem ancri 552
 Description: Deduction conjoining antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.)
Hypothesis
Ref Expression
ancri.1 (𝜑𝜓)
Assertion
Ref Expression
ancri (𝜑 → (𝜓𝜑))

Proof of Theorem ancri
StepHypRef Expression
1 ancri.1 . 2 (𝜑𝜓)
2 id 22 . 2 (𝜑𝜑)
31, 2jca 514 1 (𝜑 → (𝜓𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398 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 209  df-an 399 This theorem is referenced by:  gencbvex  3548  eusv2nf  5286  trsuc  6268  fo00  6643  eqfnov2  7273  caovmo  7377  bropopvvv  7777  tz7.48lem  8069  tz7.48-1  8071  oewordri  8210  epfrs  9165  ordpipq  10356  ltexprlem4  10453  xrinfmsslem  12693  hashfzp1  13784  dfgcd2  15886  catpropd  16971  symg2bas  18513  psgndiflemB  20736  pmatcollpw2lem  21377  icccvx  23546  uspgr1v1eop  27023  esumcst  31310  ddemeas  31483  bnj600  32179  bnj852  32181  satfvsucsuc  32600  satffunlem2lem2  32641  satffunlem2  32643  dfpo2  32979  bj-csbsnlem  34208  bj-elid6  34448  nzss  40629  iotasbc  40731  wallispilem3  42332  dfafv2  43311  nnsum3primes4  43933  idmgmhm  44035
 Copyright terms: Public domain W3C validator