MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpbir3and Structured version   Visualization version   GIF version

Theorem mpbir3and 1435
Description: Detach a conjunction of truths in a biconditional. (Contributed by Mario Carneiro, 11-May-2014.) (Revised by Mario Carneiro, 9-Jan-2015.)
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 1151 . 2 (𝜑 → (𝜒𝜃𝜏))
5 mpbir3and.4 . 2 (𝜑 → (𝜓 ↔ (𝜒𝜃𝜏)))
64, 5mpbird 248 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  w3a 1100
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 198  df-an 385  df-3an 1102
This theorem is referenced by:  canthwelem  9753  intwun  9838  tskwun  9887  gruwun  9916  ixxss1  12407  ixxss2  12408  ixxss12  12409  ixxub  12410  ixxlb  12411  elicod  12438  ubioc1  12441  lbico1  12442  lbicc2  12504  ubicc2  12505  difreicc  12523  supicc  12539  modelico  12900  zmodfz  12912  addmodid  12938  dfrtrcl2  14021  phicl2  15686  4sqlem12  15873  isfuncd  16725  idfucl  16741  cofucl  16748  invfuc  16834  cnvps  17413  psss  17415  issubmd  17550  submid  17552  subsubm  17558  mhmima  17564  mhmeql  17565  gsumwspan  17584  frmdsssubm  17599  issubgrpd2  17808  grpissubg  17812  subgint  17816  0subg  17817  cycsubgcl  17818  nmzsubg  17833  eqger  17842  eqgcpbl  17846  ghmrn  17871  ghmpreima  17880  gastacl  17939  cntzsubm  17965  sylow2blem1  18232  lsmsubm  18265  torsubg  18454  oddvdssubg  18455  dmdprdd  18596  dprdsubg  18621  dprdres  18625  unitsubm  18868  subrgsubm  18993  subrgugrp  18999  subrgint  19002  issubdrg  19005  cntzsubr  19012  lsssubg  19160  islmhm2  19241  pj1lmhm  19303  islbs2  19359  islbs3  19360  lbsextlem4  19366  issubrngd2  19394  lidlsubg  19420  2idlcpbl  19439  mplsubglem  19639  mplsubrg  19645  mplind  19706  isphld  20205  dmatsgrp  20512  dmatsrng  20514  scmatsgrp  20532  scmatsrng  20533  scmatsgrp1  20535  scmatsrng1  20536  cpmatsubgpmat  20734  cpmatsrgpmat  20735  lmcnp  21318  isufil2  21921  ufileu  21932  filufint  21933  fmfnfm  21971  flimclslem  21997  fclsfnflim  22040  flimfnfcls  22041  fclscmp  22043  clssubg  22121  tgpconncompeqg  22124  tgpconncomp  22125  qustgpopn  22132  tgptsmscls  22162  xmeter  22447  metust  22572  tgqioo  22812  zcld  22825  iccntr  22833  icccmplem2  22835  icccmplem3  22836  reconnlem1  22838  reconnlem2  22839  xrge0tsms  22846  cnheiborlem  22962  om1addcl  23041  pi1blem  23047  pi1grplem  23057  pi1inv  23060  pi1xfr  23063  pi1xfrcnvlem  23064  pi1coghm  23069  cmetcaulem  23294  ivthlem2  23429  ivthlem3  23430  ovolicc2lem2  23495  ovolicc2lem5  23498  opnmbllem  23578  volcn  23583  ismbf3d  23631  mbfi1fseqlem6  23697  itg2const2  23718  i1fibl  23784  ibladd  23797  ditgsplitlem  23834  dvferm1lem  23957  dvferm2lem  23959  dvlip2  23968  dvivthlem1  23981  dvne0  23984  lhop1lem  23986  lhop1  23987  lhop  23989  dvcnvrelem1  23990  dvcnvrelem2  23991  dvcnvre  23992  ftc1lem1  24008  itgsubst  24022  aaliou3lem2  24308  psercnlem2  24388  efif1olem2  24500  logtayl  24616  log2tlbnd  24882  xrlimcnp  24905  pntibndlem2  25490  pntlemj  25502  pntleml  25510  trgcgr  25621  axlowdim  26051  uhgrissubgr  26379  egrsubgr  26381  uhgrspansubgr  26395  uhgrspan1  26407  cusgrrusgr  26701  wlkonwlk  26782  wlkonwlk1l  26783  wlkres  26791  wlkp1  26802  wlkd  26807  lfgriswlk  26809  wwlksnextinj  27032  2wlkond  27073  wpthswwlks2on  27098  wpthswwlks2onOLD  27099  0wlkon  27289  1wlkd  27310  1pthond  27313  eliccelico  29862  elicoelioo  29863  xrge0tsmsd  30106  tpr2rico  30279  measinb  30605  cntmeas  30610  dya2icoseg  30660  sibf0  30717  sibfof  30723  resconn  31546  cvmsss2  31574  cvmliftlem10  31594  mrsubco  31736  cgrextend  32431  cgr3rflx  32477  cgrxfr  32478  btwnconn1lem4  32513  btwnconn1lem8  32517  btwnconn1lem11  32520  bj-pinftynminfty  33426  iooelexlt  33521  opnmbllem0  33753  ibladdnc  33774  bddiblnc  33787  ftc1anc  33800  isbnd3  33889  prdsbnd  33898  rngomndo  34040  isgrpda  34060  rngohomco  34079  rngoisocnv  34086  rngoidl  34129  0idl  34130  intidl  34134  unichnidl  34136  keridl  34137  smprngopr  34157  lshpnel2N  34760  lkrshp  34880  4atexlemex2  35846  4atex  35851  cdleme0moN  36000  istendod  36537  dihlspsnat  37108  dochsatshp  37226  mon1psubm  38279  iocinico  38291  dfrtrcl3  38519  eliood  40198  eliccd  40204  eliocd  40208  limciccioolb  40327  limcicciooub  40343  icccncfext  40574  iblspltprt  40662  itgspltprt  40668  fourierdlem1  40798  fourierdlem4  40801  fourierdlem32  40829  fourierdlem33  40830  fourierdlem43  40840  fourierdlem65  40861  fourierdlem79  40875  issald  41024  iccpartrn  41935  bgoldbtbnd  42266  expnegico01  42870  dignnld  42959
  Copyright terms: Public domain W3C validator