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

Theorem biantru 300
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 298 . 2  |-  ( ph  ->  ( ps  <->  ( ps  /\ 
ph ) ) )
31, 2ax-mp 5 1  |-  ( ps  <->  ( ps  /\  ph )
)
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm4.71  387  mpbiran2  926  isset  2718  rexcom4b  2737  eueq  2883  ssrabeq  3214  a9evsep  4086  pwunim  4246  elvv  4648  elvvv  4649  resopab  4910  funfn  5200  dffn2  5321  dffn3  5330  dffn4  5398  fsn  5639  ixp0x  6671  ac6sfi  6843  fimax2gtri  6846  xrmaxiflemcom  11146  trirec0xor  13616
  Copyright terms: Public domain W3C validator