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

Theorem mpbir2an 848
Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.) (Revised by NM, 9-Jan-2015.)
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 846 . 2 (φχ)
51, 4mpbir 134 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:  3pm3.2i  1081  euequ1  1992  eqssi  2955  dtruarb  3933  opnzi  3963  so0  4054  ord0  4094  ordon  4178  onsucelsucexmidlem1  4213  regexmidlemm  4217  ordpwsucexmid  4246  ordom  4272  funi  4875  funcnvsn  4888  fnresi  4959  fn0  4961  f0  5023  fconst  5025  f10  5103  f1o0  5106  f1oi  5107  f1osn  5109  isoid  5393  acexmidlem2  5452  fo1st  5726  fo2nd  5727  iordsmo  5853  tfrlem7  5874  tfrexlem  5889  1pi  6299  prarloclemcalc  6484  ltsopr  6568  ltsosr  6652  axicn  6709  ltso  6853  nnind  7671  0z  7992  dfuzi  8084  cnref1o  8317  elrpii  8321  xrltso  8447  0e0icopnf  8578  0e0iccpnf  8579  expcl2lemap  8881  expclzaplem  8893  expge0  8905  expge1  8906  bj-indint  9320  bj-omord  9346
  Copyright terms: Public domain W3C validator