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 554 1 (𝜑 → (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 386
This theorem is referenced by:  bamalip  2585  gencbvex  3236  eusv2nf  4824  issref  5468  trsuc  5769  fo00  6129  eqfnov2  6720  caovmo  6824  bropopvvv  7200  tz7.48lem  7481  tz7.48-1  7483  oewordri  7617  epfrs  8551  ordpipq  9708  ltexprlem4  9805  xrinfmsslem  12081  hashfzp1  13158  swrdccat3a  13431  dfgcd2  15187  catpropd  16290  idmhm  17265  symg2bas  17739  psgndiflemB  19865  pmatcollpw2lem  20501  icccvx  22657  uspgr1v1eop  26034  esumcst  29906  ddemeas  30080  bnj600  30697  bnj852  30699  dfpo2  31353  bj-csbsnlem  32545  nzss  37998  iotasbc  38102  wallispilem3  39591  nnsum3primes4  40965  idmgmhm  41076
  Copyright terms: Public domain W3C validator