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

Theorem mpbir3and 1098
 Description: Detach a conjunction of truths in a biconditional. (Contributed by Mario Carneiro, 11-May-2014.)
Hypotheses
Ref Expression
mpbir3and.1 (𝜑𝜒)
mpbir3and.2 (𝜑𝜃)
mpbir3and.3 (𝜑𝜏)
mpbir3and.4 (𝜑 → (𝜓 ↔ (𝜒𝜃𝜏)))
Assertion
Ref Expression
mpbir3and (𝜑𝜓)

Proof of Theorem mpbir3and
StepHypRef Expression
1 mpbir3and.1 . . 3 (𝜑𝜒)
2 mpbir3and.2 . . 3 (𝜑𝜃)
3 mpbir3and.3 . . 3 (𝜑𝜏)
41, 2, 33jca 1095 . 2 (𝜑 → (𝜒𝜃𝜏))
5 mpbir3and.4 . 2 (𝜑 → (𝜓 ↔ (𝜒𝜃𝜏)))
64, 5mpbird 160 1 (𝜑𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102   ∧ w3a 896 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  df-3an 898 This theorem is referenced by:  ixxss1  8874  ixxss2  8875  ixxss12  8876  ubioc1  8899  lbico1  8900  lbicc2  8953  ubicc2  8954  modqelico  9284  zmodfz  9296  modqmuladdim  9317  addmodid  9322
 Copyright terms: Public domain W3C validator