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

Theorem mpbir3and 1180
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 1177 . 2 (𝜑 → (𝜒𝜃𝜏))
5 mpbir3and.4 . 2 (𝜑 → (𝜓 ↔ (𝜒𝜃𝜏)))
64, 5mpbird 167 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  ixxss1  9906  ixxss2  9907  ixxss12  9908  ubioc1  9931  lbico1  9932  lbicc2  9986  ubicc2  9987  elicod  10267  modqelico  10336  zmodfz  10348  modqmuladdim  10369  addmodid  10374  phicl2  12216  isstruct2r  12475  issubmd  12870  mndissubm  12871  submid  12873  0subm  12876  mhmima  12880  mhmeql  12881  issubgrpd2  13055  grpissubg  13059  subgintm  13063  nmzsubg  13075  eqger  13088  eqgcpbl  13092  unitsubm  13293  subrgsubm  13360  subrgugrp  13366  subrgintm  13369  islssmd  13451  lsssubg  13469  islss4  13474  lmtopcnp  13835  xmeter  14021  tgqioo  14132  suplociccreex  14187  dedekindicc  14196  ivthinclemlopn  14199  ivthinclemuopn  14201  sin0pilem2  14288  pilem3  14289  coseq0q4123  14340
  Copyright terms: Public domain W3C validator