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

Theorem mpbir3and 1182
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 1179 . 2 (𝜑 → (𝜒𝜃𝜏))
5 mpbir3and.4 . 2 (𝜑 → (𝜓 ↔ (𝜒𝜃𝜏)))
64, 5mpbird 167 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  w3a 980
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 982
This theorem is referenced by:  ixxss1  9922  ixxss2  9923  ixxss12  9924  ubioc1  9947  lbico1  9948  lbicc2  10002  ubicc2  10003  elicod  10283  modqelico  10352  zmodfz  10364  modqmuladdim  10385  addmodid  10390  phicl2  12232  isstruct2r  12491  issubmd  12892  mndissubm  12893  submid  12895  subsubm  12901  0subm  12902  mhmima  12909  mhmeql  12910  issubgrpd2  13095  grpissubg  13099  subgintm  13103  nmzsubg  13115  eqger  13129  eqgcpbl  13133  ghmrn  13157  ghmpreima  13166  unitsubm  13430  subrgsubm  13542  subrgugrp  13548  subrgintm  13551  islssmd  13636  lsssubg  13654  islss4  13659  issubrgd  13729  lidlsubg  13763  2idlcpblrng  13799  lmtopcnp  14147  xmeter  14333  tgqioo  14444  suplociccreex  14499  dedekindicc  14508  ivthinclemlopn  14511  ivthinclemuopn  14513  sin0pilem2  14600  pilem3  14601  coseq0q4123  14652
  Copyright terms: Public domain W3C validator