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

Theorem ancri 546
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 508 1 (𝜑 → (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385
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 199  df-an 386
This theorem is referenced by:  bamalipOLD  2761  gencbvex  3438  eusv2nf  5065  idrefOLD  5727  trsuc  6025  fo00  6391  eqfnov2  7001  caovmo  7105  bropopvvv  7492  tz7.48lem  7775  tz7.48-1  7777  oewordri  7912  epfrs  8857  ordpipq  10052  ltexprlem4  10149  xrinfmsslem  12387  hashfzp1  13467  swrdccat3aOLD  13804  dfgcd2  15598  catpropd  16683  idmhm  17659  symg2bas  18130  psgndiflemB  20268  pmatcollpw2lem  20910  icccvx  23077  uspgr1v1eop  26483  esumcst  30641  ddemeas  30815  bnj600  31506  bnj852  31508  dfpo2  32159  bj-csbsnlem  33389  bj-ismooredr2  33558  nzss  39298  iotasbc  39401  wallispilem3  41027  dfafv2  41986  nnsum3primes4  42458  idmgmhm  42587
  Copyright terms: Public domain W3C validator