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

Theorem mpbiran2 848
 Description: Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.) (Revised by NM, 9-Jan-2015.)
Hypotheses
Ref Expression
mpbiran2.1 𝜒
mpbiran2.2 (𝜑 ↔ (𝜓𝜒))
Assertion
Ref Expression
mpbiran2 (𝜑𝜓)

Proof of Theorem mpbiran2
StepHypRef Expression
1 mpbiran2.2 . 2 (𝜑 ↔ (𝜓𝜒))
2 mpbiran2.1 . . 3 𝜒
32biantru 286 . 2 (𝜓 ↔ (𝜓𝜒))
41, 3bitr4i 176 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:  reueq  2738  ss0b  3256  eusv1  4184  eusv2nf  4188  eusv2  4189  opthprc  4391  opelres  4617  f1cnvcnv  5100  fores  5115  f1orn  5136  funfvdm  5236  dfoprab2  5552  tpostpos  5879  opelreal  6904  elreal2  6907  eqresr  6912  axprecex  6954  bdeq0  9987
 Copyright terms: Public domain W3C validator