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

Theorem biantru 286
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
biantru.1 φ
Assertion
Ref Expression
biantru (ψ ↔ (ψ φ))

Proof of Theorem biantru
StepHypRef Expression
1 biantru.1 . 2 φ
2 iba 284 . 2 (φ → (ψ ↔ (ψ φ)))
31, 2ax-mp 7 1 (ψ ↔ (ψ φ))
Colors of variables: wff set class
Syntax hints:   wa 97  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm4.71  369  mpbiran2  847  isset  2555  rexcom4b  2573  eueq  2706  ssrabeq  3020  nsspssun  3164  disjpss  3272  a9evsep  3870  pwunim  4014  elvv  4345  elvvv  4346  resopab  4595  funfn  4874  dffn2  4990  dffn3  4996  dffn4  5055  fsn  5278
  Copyright terms: Public domain W3C validator