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

Theorem ancri 549
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 511 1 (𝜑 → (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  gencbvex  3541  eusv2nf  5395  dfpo2  6316  trsuc  6471  fo00  6884  eqfnov2  7563  caovmo  7670  bropopvvv  8115  tz7.48lem  8481  tz7.48-1  8483  oewordri  8630  epfrs  9771  ordpipq  10982  ltexprlem4  11079  xrinfmsslem  13350  hashfzp1  14470  dfgcd2  16583  catpropd  17752  idmgmhm  18714  symg2bas  19410  psgndiflemB  21618  pmatcollpw2lem  22783  icccvx  24981  uspgr1v1eop  29266  esumcst  34064  ddemeas  34237  bnj600  34933  bnj852  34935  satfvsucsuc  35370  satffunlem2lem2  35411  satffunlem2  35413  bj-csbsnlem  36904  bj-elid6  37171  aks6d1c6isolem3  42177  nzss  44336  iotasbc  44438  wallispilem3  46082  dfafv2  47144  nnsum3primes4  47775
  Copyright terms: Public domain W3C validator