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

Theorem mpbir3and 1165
 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 1162 . 2
5 mpbir3and.4 . 2
64, 5mpbird 166 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 104   w3a 963 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 965 This theorem is referenced by:  ixxss1  9716  ixxss2  9717  ixxss12  9718  ubioc1  9741  lbico1  9742  lbicc2  9796  ubicc2  9797  modqelico  10137  zmodfz  10149  modqmuladdim  10170  addmodid  10175  phicl2  11924  isstruct2r  12007  lmtopcnp  12456  xmeter  12642  tgqioo  12753  suplociccreex  12808  dedekindicc  12817  ivthinclemlopn  12820  ivthinclemuopn  12822  sin0pilem2  12909  pilem3  12910  coseq0q4123  12961
 Copyright terms: Public domain W3C validator