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

Theorem mpbir3and 1169
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 1166 . 2 (𝜑 → (𝜒𝜃𝜏))
5 mpbir3and.4 . 2 (𝜑 → (𝜓 ↔ (𝜒𝜃𝜏)))
64, 5mpbird 166 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  w3a 967
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 969
This theorem is referenced by:  ixxss1  9834  ixxss2  9835  ixxss12  9836  ubioc1  9859  lbico1  9860  lbicc2  9914  ubicc2  9915  elicod  10194  modqelico  10263  zmodfz  10275  modqmuladdim  10296  addmodid  10301  phicl2  12140  isstruct2r  12399  lmtopcnp  12848  xmeter  13034  tgqioo  13145  suplociccreex  13200  dedekindicc  13209  ivthinclemlopn  13212  ivthinclemuopn  13214  sin0pilem2  13301  pilem3  13302  coseq0q4123  13353
  Copyright terms: Public domain W3C validator