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

Theorem mpbir2an 860
 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 858 . 2 (𝜑𝜒)
51, 4mpbir 138 1 𝜑
 Colors of variables: wff set class Syntax hints:   ∧ wa 101   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  3pm3.2i  1093  euequ1  2011  eqssi  2989  dtruarb  3970  opnzi  4000  so0  4091  we0  4126  ord0  4156  ordon  4240  onsucelsucexmidlem1  4281  regexmidlemm  4285  ordpwsucexmid  4322  reg3exmidlemwe  4331  ordom  4357  funi  4960  funcnvsn  4973  fnresi  5044  fn0  5046  f0  5108  fconst  5110  f10  5188  f1o0  5191  f1oi  5192  f1osn  5194  isoid  5478  acexmidlem2  5537  fo1st  5812  fo2nd  5813  iordsmo  5943  tfrlem7  5964  tfrexlem  5979  1pi  6471  prarloclemcalc  6658  ltsopr  6752  ltsosr  6907  axicn  6997  nnindnn  7025  ltso  7155  nnind  8006  0z  8313  dfuzi  8407  cnref1o  8680  elrpii  8684  xrltso  8818  0e0icopnf  8949  0e0iccpnf  8950  fldiv4p1lem1div2  9255  expcl2lemap  9432  expclzaplem  9444  expge0  9456  expge1  9457  fclim  10046  halfleoddlt  10206  ex-fl  10279  bj-indint  10442  bj-omord  10472
 Copyright terms: Public domain W3C validator