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

Theorem ancri 553
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 515 1 (𝜑 → (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  gencbvex  3469  eusv2nf  5293  trsuc  6302  fo00  6701  eqfnov2  7345  caovmo  7450  bropopvvv  7863  tz7.48lem  8182  tz7.48-1  8184  oewordri  8325  epfrs  9352  ordpipq  10561  ltexprlem4  10658  xrinfmsslem  12903  hashfzp1  14003  dfgcd2  16111  catpropd  17217  symg2bas  18790  psgndiflemB  20567  pmatcollpw2lem  21679  icccvx  23852  uspgr1v1eop  27342  esumcst  31748  ddemeas  31921  bnj600  32617  bnj852  32619  satfvsucsuc  33045  satffunlem2lem2  33086  satffunlem2  33088  dfpo2  33446  bj-csbsnlem  34830  bj-elid6  35081  nzss  41616  iotasbc  41718  wallispilem3  43291  dfafv2  44304  nnsum3primes4  44921  idmgmhm  45023
  Copyright terms: Public domain W3C validator