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

Theorem mpbir2an 884
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  |-  ps
mpbir2an.2  |-  ch
mpbiran2an.1  |-  ( ph  <->  ( ps  /\  ch )
)
Assertion
Ref Expression
mpbir2an  |-  ph

Proof of Theorem mpbir2an
StepHypRef Expression
1 mpbir2an.2 . 2  |-  ch
2 mpbir2an.1 . . 3  |-  ps
3 mpbiran2an.1 . . 3  |-  ( ph  <->  ( ps  /\  ch )
)
42, 3mpbiran 882 . 2  |-  ( ph  <->  ch )
51, 4mpbir 144 1  |-  ph
Colors of variables: wff set class
Syntax hints:    /\ wa 102    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  3pm3.2i  1117  euequ1  2037  eqssi  3016  elini  3157  dtruarb  3970  opnzi  3998  so0  4089  we0  4124  ord0  4154  ordon  4238  onsucelsucexmidlem1  4279  regexmidlemm  4283  ordpwsucexmid  4321  reg3exmidlemwe  4329  ordom  4355  funi  4962  funcnvsn  4975  funinsn  4979  fnresi  5047  fn0  5049  f0  5111  fconst  5113  f10  5191  f1o0  5194  f1oi  5195  f1osn  5197  isoid  5481  acexmidlem2  5540  fo1st  5815  fo2nd  5816  iordsmo  5946  tfrlem7  5966  tfrexlem  5983  1domsn  6363  1pi  6567  prarloclemcalc  6754  ltsopr  6848  ltsosr  7003  axicn  7093  nnindnn  7121  ltso  7256  negiso  8100  nnind  8122  0z  8443  dfuzi  8538  cnref1o  8814  elrpii  8818  xrltso  8947  0e0icopnf  9078  0e0iccpnf  9079  fldiv4p1lem1div2  9387  expcl2lemap  9585  expclzaplem  9597  expge0  9609  expge1  9610  fclim  10271  halfleoddlt  10438  2prm  10653  3prm  10654  ex-fl  10714  bj-indint  10884  bj-omord  10913
  Copyright terms: Public domain W3C validator