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

Theorem ancld 318
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  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
ancld  |-  ( ph  ->  ( ps  ->  ( ps  /\  ch ) ) )

Proof of Theorem ancld
StepHypRef Expression
1 idd 21 . 2  |-  ( ph  ->  ( ps  ->  ps ) )
2 ancld.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2jcad 301 1  |-  ( ph  ->  ( ps  ->  ( ps  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  mopick2  2031  cgsexg  2654  cgsex2g  2655  cgsex4g  2656  reximdva0m  3296  difsn  3569  preq12b  3609  elres  4735  relssres  4737  fnoprabg  5728  1idprl  7128  1idpru  7129  msqge0  8069  mulge0  8072  fzospliti  9552  ialgcvga  11115  prmind2  11184  sqrt2irr  11223
  Copyright terms: Public domain W3C validator