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

Theorem biantru 296
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
biantru.1  |-  ph
Assertion
Ref Expression
biantru  |-  ( ps  <->  ( ps  /\  ph )
)

Proof of Theorem biantru
StepHypRef Expression
1 biantru.1 . 2  |-  ph
2 iba 294 . 2  |-  ( ph  ->  ( ps  <->  ( ps  /\ 
ph ) ) )
31, 2ax-mp 7 1  |-  ( ps  <->  ( ps  /\  ph )
)
Colors of variables: wff set class
Syntax hints:    /\ wa 102    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm4.71  381  mpbiran2  887  isset  2625  rexcom4b  2644  eueq  2786  ssrabeq  3107  a9evsep  3961  pwunim  4113  elvv  4500  elvvv  4501  resopab  4756  funfn  5045  dffn2  5163  dffn3  5171  dffn4  5239  fsn  5469  ac6sfi  6612  fimax2gtri  6615
  Copyright terms: Public domain W3C validator