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

Theorem mpbir3and 1164
 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 1161 . 2 (𝜑 → (𝜒𝜃𝜏))
5 mpbir3and.4 . 2 (𝜑 → (𝜓 ↔ (𝜒𝜃𝜏)))
64, 5mpbird 166 1 (𝜑𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104   ∧ w3a 962 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  df-3an 964 This theorem is referenced by:  ixxss1  9699  ixxss2  9700  ixxss12  9701  ubioc1  9724  lbico1  9725  lbicc2  9779  ubicc2  9780  modqelico  10119  zmodfz  10131  modqmuladdim  10152  addmodid  10157  phicl2  11901  isstruct2r  11984  lmtopcnp  12433  xmeter  12619  tgqioo  12730  suplociccreex  12785  dedekindicc  12794  ivthinclemlopn  12797  ivthinclemuopn  12799  sin0pilem2  12885  pilem3  12886  coseq0q4123  12937
 Copyright terms: Public domain W3C validator