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  4700  elrnmpt1  4880  fliftf  5802  elxp7  6173  eroveu  6628  sbthlemi5  6962  sbthlemi6  6963  elfi2  6973  reapltxor  8548  divap0b  8642  nnle1eq1  8945  nn0le0eq0  9206  nn0lt10b  9335  ioopos  9952  xrmaxiflemcom  11259  fz1f1o  11385  nndivdvds  11805  dvdsmultr2  11842  pcmpt  12343  pcmpt2  12344  lssle0  13463  discld  13675  cncnpi  13767  cnptoprest2  13779  lmss  13785  txcn  13814  isxmet2d  13887  xblss2  13944  bdxmet  14040  xmetxp  14046  cncfcdm  14108  lgsneg  14464  lgsdilem  14467
  Copyright terms: Public domain W3C validator