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

Theorem ancld 312
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 295 1 (𝜑 → (𝜓 → (𝜓𝜒)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105
This theorem is referenced by:  mopick2  1999  cgsexg  2606  cgsex2g  2607  cgsex4g  2608  reximdva0m  3264  difsn  3529  preq12b  3569  elres  4674  relssres  4676  fnoprabg  5630  1idprl  6746  1idpru  6747  msqge0  7681  mulge0  7684  fzospliti  9134  sqrt2irr  10251  ialgcvga  10273
  Copyright terms: Public domain W3C validator