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

Theorem mpbir2an 909
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 907 . 2  |-  ( ph  <->  ch )
51, 4mpbir 145 1  |-  ph
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  3pm3.2i  1142  euequ1  2070  eqssi  3081  elini  3228  dtruarb  4083  opnzi  4125  so0  4216  we0  4251  ord0  4281  ordon  4370  onsucelsucexmidlem1  4411  regexmidlemm  4415  ordpwsucexmid  4453  reg3exmidlemwe  4461  ordom  4488  funi  5123  funcnvsn  5136  funinsn  5140  fnresi  5208  fn0  5210  f0  5281  fconst  5286  f10  5367  f1o0  5370  f1oi  5371  f1osn  5373  isoid  5677  iso0  5684  acexmidlem2  5737  fo1st  6021  fo2nd  6022  iordsmo  6160  tfrlem7  6180  tfrexlem  6197  mapsnf1o2  6556  1domsn  6679  inresflem  6911  0ct  6958  infnninf  6988  exmidaclem  7028  1pi  7087  prarloclemcalc  7274  ltsopr  7368  ltsosr  7536  cnm  7604  axicn  7635  axaddf  7640  axmulf  7641  nnindnn  7665  ltso  7806  negiso  8673  nnind  8696  0z  9019  dfuzi  9115  cnref1o  9392  elrpii  9396  xrltso  9533  0e0icopnf  9713  0e0iccpnf  9714  fldiv4p1lem1div2  10029  expcl2lemap  10256  expclzaplem  10268  expge0  10280  expge1  10281  xrnegiso  10982  fclim  11014  eff2  11296  reeff1  11317  ef01bndlem  11373  sin01bnd  11374  cos01bnd  11375  sin01gt0  11378  egt2lt3  11393  halfleoddlt  11498  2prm  11715  3prm  11716  setsslnid  11916  fntopon  12097  istpsi  12112  ismeti  12421  tgqioo  12622  addcncntoplem  12626  divcnap  12630  abscncf  12647  recncf  12648  imcncf  12649  cjcncf  12650  dveflem  12761  ex-fl  12771  bj-indint  12963  bj-omord  12992  0nninf  13031  peano4nninf  13034  isomninnlem  13059
  Copyright terms: Public domain W3C validator