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

Theorem ancri 576
 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 555 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 197  df-an 385 This theorem is referenced by:  bamalip  2724  gencbvex  3390  eusv2nf  5013  issref  5667  trsuc  5971  fo00  6334  eqfnov2  6933  caovmo  7037  bropopvvv  7424  tz7.48lem  7706  tz7.48-1  7708  oewordri  7843  epfrs  8782  ordpipq  9976  ltexprlem4  10073  xrinfmsslem  12351  hashfzp1  13430  swrdccat3a  13714  dfgcd2  15485  catpropd  16590  idmhm  17565  symg2bas  18038  psgndiflemB  20168  pmatcollpw2lem  20804  icccvx  22970  uspgr1v1eop  26361  esumcst  30455  ddemeas  30629  bnj600  31317  bnj852  31319  dfpo2  31973  bj-csbsnlem  33220  bj-ismooredr2  33389  nzss  39036  iotasbc  39140  wallispilem3  40805  nnsum3primes4  42204  idmgmhm  42316
 Copyright terms: Public domain W3C validator