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  837  isset  2538  rexcom4b  2555  eueq  2688  ssrabeq  3005  nsspssun  3149  disjpss  3257  a9evsep  3832  pwunim  3977  elvv  4305  elvvv  4306  resopab  4556  funfn  4834  dffn2  4950  dffn3  4956  dffn4  5014  fsn  5237
  Copyright terms: Public domain W3C validator