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

Theorem mpbir2an 837
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 835 . 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  1067  euequ1  1977  eqssi  2938  dtruarb  3916  opnzi  3946  so0  4037  ord0  4077  ordon  4162  onsucelsucexmidlem1  4197  regexmidlemm  4201  ordpwsucexmid  4230  ordom  4256  funi  4858  funcnvsn  4871  fnresi  4942  fn0  4944  f0  5005  fconst  5007  f10  5085  f1o0  5088  f1oi  5089  f1osn  5091  isoid  5375  acexmidlem2  5433  fo1st  5707  fo2nd  5708  iordsmo  5834  tfrlem7  5855  tfrexlem  5870  tfri1  5873  1pi  6175  prarloclemcalc  6356  ltsopr  6433  ltsosr  6511  axicn  6559  ltso  6696  bj-indint  7301  bj-omord  7327
  Copyright terms: Public domain W3C validator