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

Theorem ancri 573
 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 553 1 (𝜑 → (𝜓𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  bamalip  2574  gencbvex  3223  eusv2nf  4790  issref  5428  trsuc  5727  fo00  6084  eqfnov2  6665  caovmo  6769  bropopvvv  7142  tz7.48lem  7423  tz7.48-1  7425  oewordri  7559  epfrs  8490  ordpipq  9643  ltexprlem4  9740  xrinfmsslem  12010  hashfzp1  13078  swrdccat3a  13345  dfgcd2  15101  catpropd  16192  idmhm  17167  symg2bas  17641  psgndiflemB  19765  pmatcollpw2lem  20401  icccvx  22557  0wlkon  26077  2wlkonot3v  26402  2spthonot3v  26403  esumcst  29452  ddemeas  29626  bnj600  30243  bnj852  30245  dfpo2  30898  bj-csbsnlem  32090  nzss  37538  iotasbc  37642  wallispilem3  38960  nnsum3primes4  40204  uspgr1v1eop  40475  idmgmhm  41578
 Copyright terms: Public domain W3C validator