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

Theorem ancld 308
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 291 1  |-  ( ph  ->  ( ps  ->  ( ps  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101
This theorem is referenced by:  mopick2  1983  cgsexg  2589  cgsex2g  2590  cgsex4g  2591  reximdva0m  3236  difsn  3501  preq12b  3541  elres  4646  relssres  4648  fnoprabg  5602  1idprl  6688  1idpru  6689  msqge0  7607  mulge0  7610  fzospliti  9032  sqrt2irr  9878  ialgcvga  9890
  Copyright terms: Public domain W3C validator