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  2082  cgsexg  2721  cgsex2g  2722  cgsex4g  2723  reximdva0m  3378  difsn  3657  preq12b  3697  elres  4855  relssres  4857  fnoprabg  5872  1idprl  7410  1idpru  7411  msqge0  8390  mulge0  8393  fzospliti  9965  algcvga  11743  prmind2  11812  sqrt2irr  11851  metrest  12689
  Copyright terms: Public domain W3C validator