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