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

Theorem mpbi2and 945
Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Hypotheses
Ref Expression
mpbi2and.1 (𝜑𝜓)
mpbi2and.2 (𝜑𝜒)
mpbi2and.3 (𝜑 → ((𝜓𝜒) ↔ 𝜃))
Assertion
Ref Expression
mpbi2and (𝜑𝜃)

Proof of Theorem mpbi2and
StepHypRef Expression
1 mpbi2and.1 . . 3 (𝜑𝜓)
2 mpbi2and.2 . . 3 (𝜑𝜒)
31, 2jca 306 . 2 (𝜑 → (𝜓𝜒))
4 mpbi2and.3 . 2 (𝜑 → ((𝜓𝜒) ↔ 𝜃))
53, 4mpbid 147 1 (𝜑𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  supisoti  7040  remim  10904  resqrtcl  11073  divalgmod  11967  oddpwdclemxy  12204  divnumden  12231  numdensq  12237  prmdivdiv  12272  4sqlem7  12419  ismgmid2  12859  mnd1  12922  iscmnd  13254  imasring  13431  subrg1  13595  topgele  14006  lmcn2  14257
  Copyright terms: Public domain W3C validator