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

Theorem biantru 290
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 288 . 2 (𝜑 → (𝜓 ↔ (𝜓𝜑)))
31, 2ax-mp 7 1 (𝜓 ↔ (𝜓𝜑))
Colors of variables: wff set class
Syntax hints:  wa 101  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  pm4.71  375  mpbiran2  859  isset  2578  rexcom4b  2596  eueq  2735  ssrabeq  3054  nsspssun  3198  disjpss  3306  a9evsep  3907  pwunim  4051  elvv  4430  elvvv  4431  resopab  4680  funfn  4959  dffn2  5075  dffn3  5081  dffn4  5140  fsn  5363  ac6sfi  6383
  Copyright terms: Public domain W3C validator