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

Theorem mpbir2an 926
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 924 . 2 (𝜑𝜒)
51, 4mpbir 145 1 𝜑
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  1159  euequ1  2094  eqssi  3113  elini  3260  dtruarb  4115  opnzi  4157  so0  4248  we0  4283  ord0  4313  ordon  4402  onsucelsucexmidlem1  4443  regexmidlemm  4447  ordpwsucexmid  4485  reg3exmidlemwe  4493  ordom  4520  funi  5155  funcnvsn  5168  funinsn  5172  fnresi  5240  fn0  5242  f0  5313  fconst  5318  f10  5401  f1o0  5404  f1oi  5405  f1osn  5407  isoid  5711  iso0  5718  acexmidlem2  5771  fo1st  6055  fo2nd  6056  iordsmo  6194  tfrlem7  6214  tfrexlem  6231  mapsnf1o2  6590  1domsn  6713  inresflem  6945  0ct  6992  infnninf  7022  exmidonfinlem  7054  exmidaclem  7069  1pi  7135  prarloclemcalc  7322  ltsopr  7416  ltsosr  7584  cnm  7652  axicn  7683  axaddf  7688  axmulf  7689  nnindnn  7713  ltso  7854  negiso  8725  nnind  8748  0z  9077  dfuzi  9173  cnref1o  9452  elrpii  9456  xrltso  9594  0e0icopnf  9774  0e0iccpnf  9775  fldiv4p1lem1div2  10090  expcl2lemap  10317  expclzaplem  10329  expge0  10341  expge1  10342  xrnegiso  11043  fclim  11075  eff2  11398  reeff1  11418  ef01bndlem  11474  sin01bnd  11475  cos01bnd  11476  sin01gt0  11479  egt2lt3  11497  halfleoddlt  11602  2prm  11819  3prm  11820  setsslnid  12024  fntopon  12205  istpsi  12220  ismeti  12529  tgqioo  12730  addcncntoplem  12734  divcnap  12738  abscncf  12755  recncf  12756  imcncf  12757  cjcncf  12758  dveflem  12870  reeff1o  12877  reefiso  12881  ioocosf1o  12957  ex-fl  13021  bj-indint  13213  bj-omord  13242  0nninf  13283  peano4nninf  13286  isomninnlem  13311  taupi  13330
  Copyright terms: Public domain W3C validator