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

Theorem ancri 557
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 519 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 209  df-an 400
This theorem is referenced by:  gencbvex  3509  eusv2nf  5349  dfpo2  6278  trsuc  6430  fo00  6838  eqfnov2  7521  caovmo  7628  bropopvvv  8063  tz7.48lem  8406  tz7.48-1  8408  oewordri  8556  epfrs  9680  ordpipq  10894  ltexprlem4  10991  xrinfmsslem  13305  hashfzp1  14438  dfgcd2  16571  catpropd  17732  idmgmhm  18726  symg2bas  19424  psgndiflemB  21640  pmatcollpw2lem  22825  icccvx  25000  uspgr1v1eop  29407  esumcst  34321  ddemeas  34494  bnj600  35175  bnj852  35177  satfvsucsuc  35676  satffunlem2lem2  35717  satffunlem2  35719  bj-csbsnlem  37349  bj-elid6  37623  aks6d1c6isolem3  42754  nzss  44854  iotasbc  44956  wallispilem3  46602  dfafv2  47687  nnsum3primes4  48371
  Copyright terms: Public domain W3C validator