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  4716  elrnmpt1  4896  fliftf  5821  elxp7  6196  eroveu  6653  sbthlemi5  6991  sbthlemi6  6992  elfi2  7002  reapltxor  8577  divap0b  8671  nnle1eq1  8974  nn0le0eq0  9235  nn0lt10b  9364  ioopos  9982  xrmaxiflemcom  11292  fz1f1o  11418  nndivdvds  11838  dvdsmultr2  11875  pcmpt  12378  pcmpt2  12379  lssle0  13705  discld  14113  cncnpi  14205  cnptoprest2  14217  lmss  14223  txcn  14252  isxmet2d  14325  xblss2  14382  bdxmet  14478  xmetxp  14484  cncfcdm  14546  lgsneg  14903  lgsdilem  14906
  Copyright terms: Public domain W3C validator