ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ancld GIF version

Theorem ancld 323
Description: Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.)
Hypothesis
Ref Expression
ancld.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
ancld (𝜑 → (𝜓 → (𝜓𝜒)))

Proof of Theorem ancld
StepHypRef Expression
1 idd 21 . 2 (𝜑 → (𝜓𝜓))
2 ancld.1 . 2 (𝜑 → (𝜓𝜒))
31, 2jcad 305 1 (𝜑 → (𝜓 → (𝜓𝜒)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  mopick2  2102  cgsexg  2765  cgsex2g  2766  cgsex4g  2767  reximdva0m  3429  difsn  3715  preq12b  3755  elres  4925  relssres  4927  fnoprabg  5951  1idprl  7539  1idpru  7540  msqge0  8522  mulge0  8525  fzospliti  10119  algcvga  11992  prmind2  12061  sqrt2irr  12103  metrest  13221  2sqlem10  13676
  Copyright terms: Public domain W3C validator