ILE Home 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  |-  ( ph  ->  ch )
mpbir3and.2  |-  ( ph  ->  th )
mpbir3and.3  |-  ( ph  ->  ta )
mpbir3and.4  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th  /\  ta )
) )
Assertion
Ref Expression
mpbir3and  |-  ( ph  ->  ps )

Proof of Theorem mpbir3and
StepHypRef Expression
1 mpbir3and.1 . . 3  |-  ( ph  ->  ch )
2 mpbir3and.2 . . 3  |-  ( ph  ->  th )
3 mpbir3and.3 . . 3  |-  ( ph  ->  ta )
41, 2, 33jca 1162 . 2  |-  ( ph  ->  ( ch  /\  th  /\  ta ) )
5 mpbir3and.4 . 2  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th  /\  ta )
) )
64, 5mpbird 166 1  |-  ( ph  ->  ps )
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