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

Theorem biantrud 304
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2013.)
Hypothesis
Ref Expression
biantrud.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
biantrud  |-  ( ph  ->  ( ch  <->  ( ch  /\ 
ps ) ) )

Proof of Theorem biantrud
StepHypRef Expression
1 biantrud.1 . 2  |-  ( ph  ->  ps )
2 iba 300 . 2  |-  ( ps 
->  ( ch  <->  ( ch  /\ 
ps ) ) )
31, 2syl 14 1  |-  ( ph  ->  ( ch  <->  ( ch  /\ 
ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  mpbiran2d  442  posng  4698  elrnmpt1  4878  fliftf  5799  elxp7  6170  eroveu  6625  sbthlemi5  6959  sbthlemi6  6960  elfi2  6970  reapltxor  8545  divap0b  8639  nnle1eq1  8942  nn0le0eq0  9203  nn0lt10b  9332  ioopos  9949  xrmaxiflemcom  11256  fz1f1o  11382  nndivdvds  11802  dvdsmultr2  11839  pcmpt  12340  pcmpt2  12341  discld  13606  cncnpi  13698  cnptoprest2  13710  lmss  13716  txcn  13745  isxmet2d  13818  xblss2  13875  bdxmet  13971  xmetxp  13977  cncfcdm  14039  lgsneg  14395  lgsdilem  14398
  Copyright terms: Public domain W3C validator