New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  mpbiran GIF version

Theorem mpbiran 884
 Description: Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.)
Hypotheses
Ref Expression
mpbiran.1 ψ
mpbiran.2 (φ ↔ (ψ χ))
Assertion
Ref Expression
mpbiran (φχ)

Proof of Theorem mpbiran
StepHypRef Expression
1 mpbiran.2 . 2 (φ ↔ (ψ χ))
2 mpbiran.1 . . 3 ψ
32biantrur 492 . 2 (χ ↔ (ψ χ))
41, 3bitr4i 243 1 (φχ)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 176   ∧ wa 358 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177  df-an 360 This theorem is referenced by:  mpbir2an  886  pm5.63  890  ddif  3398  dfun2  3490  dfin2  3491  0pss  3588  pssv  3590  disj4  3599  cnvkexg  4286  ssetkex  4294  sikexg  4296  ins2kexg  4305  ins3kexg  4306  nnsucelrlem1  4424  ncfinlowerlem1  4482  eqtfinrelk  4486  evenfinex  4503  oddfinex  4504  opabn0  4716  setconslem6  4736  fnres  5199  dmsi  5519  otelins2  5791  composeex  5820  dmpprod  5840  crossex  5850  transex  5910  enmap2  6068  csucex  6259  nmembers1lem1  6268  nchoicelem18  6306  dmfrec  6316  fnfreclem1  6317
 Copyright terms: Public domain W3C validator