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

Theorem ancri 574
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 197  df-an 385
This theorem is referenced by:  bamalip  2615  gencbvex  3281  eusv2nf  4894  issref  5544  trsuc  5848  fo00  6210  eqfnov2  6809  caovmo  6913  bropopvvv  7300  tz7.48lem  7581  tz7.48-1  7583  oewordri  7717  epfrs  8645  ordpipq  9802  ltexprlem4  9899  xrinfmsslem  12176  hashfzp1  13256  swrdccat3a  13540  dfgcd2  15310  catpropd  16416  idmhm  17391  symg2bas  17864  psgndiflemB  19994  pmatcollpw2lem  20630  icccvx  22796  uspgr1v1eop  26186  esumcst  30253  ddemeas  30427  bnj600  31115  bnj852  31117  dfpo2  31771  bj-csbsnlem  33023  bj-ismooredr2  33190  nzss  38833  iotasbc  38937  wallispilem3  40602  nnsum3primes4  42001  idmgmhm  42113
  Copyright terms: Public domain W3C validator