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

Theorem biantrud 300
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 296 . 2  |-  ( ps 
->  ( ch  <->  ( ch  /\ 
ps ) ) )
31, 2syl 14 1  |-  ( ph  ->  ( ch  <->  ( ch  /\ 
ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  mpbiran2d  436  posng  4571  elrnmpt1  4750  fliftf  5654  elxp7  6022  eroveu  6474  sbthlemi5  6801  sbthlemi6  6802  elfi2  6812  reapltxor  8266  divap0b  8353  nnle1eq1  8651  nn0le0eq0  8906  nn0lt10b  9032  ioopos  9623  xrmaxiflemcom  10907  fz1f1o  11033  nndivdvds  11344  dvdsmultr2  11378  discld  12145  cncnpi  12236  cnptoprest2  12248  lmss  12254  txcn  12283  isxmet2d  12334  xblss2  12391  bdxmet  12487  xmetxp  12493  cncffvrn  12552
  Copyright terms: Public domain W3C validator