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

Theorem ancri 551
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 513 1 (𝜑 → (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  gencbvex  3506  eusv2nf  5354  dfpo2  6252  trsuc  6408  fo00  6824  eqfnov2  7490  caovmo  7595  bropopvvv  8026  tz7.48lem  8391  tz7.48-1  8393  oewordri  8543  epfrs  9675  ordpipq  10886  ltexprlem4  10983  xrinfmsslem  13236  hashfzp1  14340  dfgcd2  16435  catpropd  17597  symg2bas  19182  psgndiflemB  21027  pmatcollpw2lem  22149  icccvx  24336  uspgr1v1eop  28246  esumcst  32726  ddemeas  32899  bnj600  33595  bnj852  33597  satfvsucsuc  34023  satffunlem2lem2  34064  satffunlem2  34066  bj-csbsnlem  35423  bj-elid6  35691  nzss  42689  iotasbc  42791  wallispilem3  44398  dfafv2  45454  nnsum3primes4  46070  idmgmhm  46172
  Copyright terms: Public domain W3C validator