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

Theorem biantru 300
 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 298 . 2 (𝜑 → (𝜓 ↔ (𝜓𝜑)))
31, 2ax-mp 5 1 (𝜓 ↔ (𝜓𝜑))
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  pm4.71  386  mpbiran2  925  isset  2692  rexcom4b  2711  eueq  2855  ssrabeq  3183  a9evsep  4050  pwunim  4208  elvv  4601  elvvv  4602  resopab  4863  funfn  5153  dffn2  5274  dffn3  5283  dffn4  5351  fsn  5592  ixp0x  6620  ac6sfi  6792  fimax2gtri  6795  xrmaxiflemcom  11030  trirec0xor  13345
 Copyright terms: Public domain W3C validator