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

Theorem mpbir2an 886
 Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.)
Hypotheses
Ref Expression
mpbir2an.1 ψ
mpbir2an.2 χ
mpbiran2an.1 (φ ↔ (ψ χ))
Assertion
Ref Expression
mpbir2an φ

Proof of Theorem mpbir2an
StepHypRef Expression
1 mpbir2an.2 . 2 χ
2 mpbir2an.1 . . 3 ψ
3 mpbiran2an.1 . . 3 (φ ↔ (ψ χ))
42, 3mpbiran 884 . 2 (φχ)
51, 4mpbir 200 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:  3pm3.2i  1130  ax12olem4  1930  euequ1  2292  eqssi  3288  sikss1c1c  4267  ins2kss  4279  ins3kss  4280  cokrelk  4284  cnvkexg  4286  ssetkex  4294  sikexg  4296  ins2kexg  4305  ins3kexg  4306  eqtfinrelk  4486  0ceven  4505  xpvv  4843  fnsn  5152  fnresi  5200  fn0  5202  f0  5248  fconst  5250  f10  5316  f1o0  5319  f1oi  5320  f1ovi  5321  f1osn  5322  fvi  5442  isoid  5490  1stfo  5505  2ndfo  5506  swapf1o  5511  xpassen  6057  2p1e3c  6156  fce  6188  0lt1c  6258  nnltp1c  6262  frecxp  6314  scancan  6331
 Copyright terms: Public domain W3C validator