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

Theorem ancri 556
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 518 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  3504  eusv2nf  5346  dfpo2  6272  trsuc  6424  fo00  6832  eqfnov2  7515  caovmo  7622  bropopvvv  8057  tz7.48lem  8400  tz7.48-1  8402  oewordri  8550  epfrs  9676  ordpipq  10890  ltexprlem4  10987  xrinfmsslem  13301  hashfzp1  14434  dfgcd2  16556  catpropd  17717  idmgmhm  18711  symg2bas  19409  psgndiflemB  21625  pmatcollpw2lem  22810  icccvx  24985  uspgr1v1eop  29389  esumcst  34314  ddemeas  34487  bnj600  35171  bnj852  35173  satfvsucsuc  35663  satffunlem2lem2  35704  satffunlem2  35706  bj-csbsnlem  37336  bj-elid6  37610  aks6d1c6isolem3  42741  nzss  44841  iotasbc  44943  wallispilem3  46589  dfafv2  47674  nnsum3primes4  48358
  Copyright terms: Public domain W3C validator