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

Theorem mpbiran2 859
 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 290 . 2 (𝜓 ↔ (𝜓𝜒))
41, 3bitr4i 180 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:  reueq  2761  ss0b  3284  eusv1  4212  eusv2nf  4216  eusv2  4217  opthprc  4419  opelres  4645  f1cnvcnv  5128  fores  5143  f1orn  5164  funfvdm  5264  dfoprab2  5580  tpostpos  5910  opelreal  6962  elreal2  6965  eqresr  6970  axprecex  7012  zeoxor  10180  bdeq0  10374
 Copyright terms: Public domain W3C validator