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  829  isset  2526  rexcom4b  2543  eueq  2676  ssrabeq  2990  nsspssun  3134  disjpss  3242  a9evsep  3838  pwunim  3982  elvv  4313  elvvv  4314  resopab  4563  funfn  4841  dffn2  4957  dffn3  4963  dffn4  5021  fsn  5244
  Copyright terms: Public domain W3C validator