MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpbir2and Unicode version

Theorem mpbir2and 888
Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Hypotheses
Ref Expression
mpbir2and.1  |-  ( ph  ->  ch )
mpbir2and.2  |-  ( ph  ->  th )
mpbir2and.3  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
Assertion
Ref Expression
mpbir2and  |-  ( ph  ->  ps )

Proof of Theorem mpbir2and
StepHypRef Expression
1 mpbir2and.1 . . 3  |-  ( ph  ->  ch )
2 mpbir2and.2 . . 3  |-  ( ph  ->  th )
31, 2jca 518 . 2  |-  ( ph  ->  ( ch  /\  th ) )
4 mpbir2and.3 . 2  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
53, 4mpbird 223 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  dffi3  7180  supmax  7212  suppr  7215  ordtypelem7  7235  cantnfle  7368  cantnf0  7372  cantnfp1lem1  7376  cantnfp1lem2  7377  cantnfp1lem3  7378  oemapvali  7382  cantnflem1a  7383  cantnflem1c  7385  cantnflem1d  7386  cantnflem1  7387  cantnf  7391  mapfien  7395  rankpwi  7491  carduni  7610  fin23lem32  7966  fpwwe2lem6  8253  fpwwe2lem9  8256  fpwwe2lem12  8259  fpwwe2lem13  8260  fpwwe2  8261  inttsk  8392  grutsk1  8439  add20  9282  supmul  9718  suprzcl  10087  uzwo3  10307  rpnnen1lem5  10342  xrre  10494  xrre3  10496  xleadd1a  10569  xlemul1a  10604  supxrre  10642  infmxrre  10650  ixxub  10673  ixxlb  10674  elioc2  10709  elico2  10710  elicc2  10711  elfz1eq  10803  fzctr  10850  fzoaddel  10902  flid  10935  flval3  10941  fladdz  10946  fldiv  10960  modid  10989  seqf1olem1  11081  bcval5  11326  hashf1lem1  11389  sqeqd  11647  sqrlem7  11730  max0add  11791  abs2difabs  11814  rddif  11820  fzomaxdiflem  11822  rexico  11833  limsupgre  11951  rlim3  11968  icco1  12010  rlimclim  12016  rlimuni  12020  rlimresb  12035  isercolllem2  12135  isercolllem3  12136  isercoll  12137  caucvgrlem  12141  caurcvgr  12142  iseraltlem3  12152  fsum00  12252  o1fsum  12267  dvdseq  12572  bitsfzolem  12621  bitsfzo  12622  bitsmod  12623  bitscmp  12625  gcd0id  12698  gcdneg  12701  bezoutlem4  12716  nn0seqcvgd  12736  prmind2  12765  qredeq  12781  isprm5  12787  hashdvds  12839  eulerthlem2  12846  pcpremul  12892  pcidlem  12920  pcgcd1  12925  pcadd2  12934  fldivp1  12941  pcfaclem  12942  prmreclem5  12963  4sqlem17  13004  vdwlem1  13024  vdwlem6  13029  vdwlem12  13035  vdwlem13  13036  0ram  13063  ram0  13065  ramub1lem1  13069  invco  13669  sectmon  13676  monsect  13677  ssctr  13698  ssceq  13699  issubc3  13719  fullsubc  13720  funcinv  13743  fthmon  13797  fuccocl  13834  fucidcl  13835  invfuc  13844  elhomai  13861  setcmon  13915  setcepi  13916  catcisolem  13934  curf2cl  14001  yonedalem4c  14047  yonedalem3  14050  yoniso  14055  isacs3lem  14265  tsrdir  14356  nmznsg  14657  ghmpreima  14700  ghmeql  14701  ghmnsgpreima  14703  cntzsubm  14807  cntzsubg  14808  cntzmhm  14810  odlem2  14850  gexlem2  14889  gexcl2  14896  sylow1lem5  14909  subgslw  14923  slwhash  14931  fislw  14932  sylow3lem1  14934  lsmsubg  14961  efgredlemd  15049  efgredlem  15052  efgcpbllemb  15060  frgpuplem  15077  cyggeninv  15166  iscygd  15170  iscygodd  15171  gsumconst  15205  gsumpt  15218  dprdfcntz  15246  eldprdi  15249  subgdmdprd  15265  subgdprd  15266  dprdpr  15281  ablfac1c  15302  ablfac1eu  15304  ablfaclem3  15318  issubdrg  15566  rhmeql  15571  rhmima  15572  cntzsubr  15573  isabvd  15581  abvdiv  15598  lsslsp  15768  lmhmima  15800  lmhmpreima  15801  lmhmeql  15808  lsmcl  15832  lspfixed  15877  issubassa  16060  issubassa2  16080  psrbaglesupp  16110  psrbaglecl  16111  psrbagaddcl  16112  psrbagcon  16113  psrbas  16120  psrlidm  16144  psrridm  16145  mvridlem  16160  mplsubglem  16175  mpllsslem  16176  mplassa  16194  subrgmpl  16200  mplcoe3  16206  mplcoe2  16207  mplbas2  16208  mplind  16239  ply1assa  16274  coe1tmmul2  16348  coe1tmmul  16349  qsssubdrg  16427  gzrngunit  16433  ocvpj  16613  distop  16729  indistopon  16734  ppttop  16740  epttop  16742  mretopd  16825  toponmre  16826  neiss  16842  opnneissb  16847  ssnei2  16849  innei  16858  ordtcld1  16923  ordtcld2  16924  lmconst  16987  cnpnei  16989  iscncl  16994  cnss1  17001  cnss2  17002  cncnpi  17003  cncnp  17005  cnconst2  17007  cnrest  17009  cnpresti  17012  cnpdis  17017  paste  17018  lmcnp  17028  cnhaus  17078  hauscmp  17130  2ndcomap  17180  1stcelcls  17183  1stccnp  17184  llyrest  17207  nllyrest  17208  llyidm  17210  nllyidm  17211  kgentopon  17229  kgenidm  17238  kgencn3  17249  txcld  17294  tx1cn  17299  tx2cn  17300  ptcld  17303  xkoccn  17309  txcnp  17310  ptcnp  17312  txcnmpt  17314  ptcn  17317  txdis1cn  17325  ptrescn  17329  txkgen  17342  xkoco1cn  17347  xkoco2cn  17348  xkococn  17350  xkoinjcn  17377  qtoptop2  17386  qtopuni  17389  qtopid  17392  qtopkgen  17397  basqtop  17398  tgqtop  17399  qtopss  17402  qtopeu  17403  qtoprest  17404  kqopn  17421  kqcld  17422  kqreglem2  17429  reghmph  17480  ordthmeolem  17488  qtopf1  17503  opnfbas  17533  isfil2  17547  fbasweak  17556  fsubbas  17558  filcon  17574  fbasrn  17575  rnelfmlem  17643  flimss2  17663  flimss1  17664  hausflim  17672  flimclslem  17675  flimsncls  17677  cnpflfi  17690  flfcnp2  17698  fclsfnflim  17718  symgtgp  17780  opnsubg  17786  ghmcnp  17793  divstgpopn  17798  divstgplem  17799  divstgphaus  17801  tsmsfbas  17806  isxmetd  17887  xmetsym  17908  imasdsf1olem  17933  imasf1oxmet  17935  xblss2  17954  xblcntr  17959  blcld  18047  ngptgp  18148  tngngpd  18165  tngnrg  18181  nlmvscn  18194  nrginvrcn  18198  nmo0  18240  nmoeq0  18241  nmoid  18247  nghmcn  18250  0nmhm  18260  blcvx  18300  zcld  18315  iccntr  18322  xrge0tsms  18335  xmetdcn2  18338  metdstri  18351  metdscn  18356  rescncf  18397  cncfco  18407  oprpiece1res2  18446  cnheibor  18449  cnllycmp  18450  bndth  18452  evth  18453  ishtpyd  18469  isphtpyd  18480  pcoval2  18510  nmhmcn  18597  ipcn  18669  lmnn  18685  cfilss  18692  iscfil3  18695  cfilfcls  18696  cmetcaulem  18710  iscmet3lem2  18714  cfilres  18718  lmcau  18734  flimcfil  18735  cncmet  18740  rlmbn  18774  minveclem3b  18788  pjthlem1  18797  pjth2  18800  ivthlem3  18809  ovolssnul  18842  ovolctb  18845  ovolunnul  18855  ovoliunnul  18862  ovolsca  18870  ovolicc  18878  ovolicopnf  18879  voliunlem2  18904  voliunlem3  18905  volsup  18909  uniioovol  18930  uniiccvol  18931  dyadmaxlem  18948  vitalilem5  18963  ismbfd  18991  mbfres  18995  mbfss  18997  mbfmulc2re  18999  mbfadd  19012  mbfmulc2  19014  mbflimsup  19017  mbflim  19019  i1faddlem  19044  i1fmullem  19045  mbfmul  19077  itg2itg1  19087  itg2seq  19093  itg2eqa  19096  itg2mulc  19098  itg2split  19100  itg2mono  19104  itg2cnlem1  19112  ibl0  19137  iblposlem  19142  itgreval  19147  iblneg  19153  iblss  19155  iblss2  19156  itgle  19160  iblconst  19168  iblabs  19179  iblabsr  19180  iblmulc2  19181  bddmulibl  19189  limciun  19240  limcun  19241  dvres2lem  19256  dvidlem  19261  dvcnp2  19265  dvcn  19266  cpnres  19282  dvaddbr  19283  dvmulbr  19284  dvcobr  19291  dvcjbr  19294  dvrec  19300  dvcnvlem  19319  dvferm  19331  dvlip2  19338  dveq0  19343  dv11cn  19344  dvivthlem1  19351  lhop1  19357  lhop2  19358  lhop  19359  dvcnvre  19362  dvfsumlem3  19371  dvfsumlem4  19372  dvfsumrlim  19374  dvfsum2  19377  ftc1a  19380  ftc1lem4  19382  ftc1lem6  19384  ftc1  19385  evlslem3  19394  mpfind  19424  coe1mul3  19481  deg1addle2  19484  deg1add  19485  deg1sublt  19492  deg1mul2  19496  deg1tm  19500  fta1blem  19550  drnguc1p  19552  ig1prsp  19559  plyco0  19570  plyeq0lem  19588  dgrub  19612  dgreq  19622  dgradd2  19645  dgrmul  19647  dgrcolem2  19651  dgrco  19652  plycpn  19665  plydivlem4  19672  plydiveu  19674  vieta1lem2  19687  vieta1  19688  aalioulem2  19709  aalioulem3  19710  aaliou3lem7  19725  tayl0  19737  ulmcn  19772  ulmdvlem3  19775  psercn  19798  abelth  19813  pilem3  19825  efif1olem1  19900  argregt0  19960  argrege0  19961  logf1o2  19993  cxpsqrlem  20045  cxpcn3  20084  abscxpbnd  20089  ang180lem2  20104  ang180lem3  20105  logreclem  20112  xrlimcnp  20259  harmonicbnd4  20300  fsumharmonic  20301  basellem3  20316  basellem4  20317  dvdsppwf1o  20422  dvdsflf1o  20423  fsumfldivdiaglem  20425  chpeq0  20443  chteq0  20444  chtub  20447  chpub  20455  dchrelbasd  20474  dchrmulcl  20484  dchrinv  20496  bcmono  20512  bposlem1  20519  bposlem2  20520  lgslem1  20531  lgsdirprm  20564  lgsqrlem2  20577  lgsqrlem3  20578  lgsdchr  20583  lgseisenlem1  20584  lgseisenlem2  20585  lgseisenlem3  20586  lgsquadlem1  20589  2sqlem8  20607  2sqblem  20612  chebbnd1lem1  20614  dchrisumlem1  20634  dchrisumlem2  20635  dchrisumlem3  20636  dchrisum0fno1  20656  pntrmax  20709  pntpbnd1a  20730  pntibndlem3  20737  pntlemn  20745  pntlemi  20749  pntlem3  20754  pntleml  20756  ostth1  20778  ostth2  20782  ostth3  20783  nvabs  21233  vacn  21261  nmcvcn  21262  nmblore  21358  0lno  21362  0blo  21364  nmlno0lem  21365  occl  21879  pjhthlem1  21966  pjpjpre  21994  nmopre  22446  nmlnop0iALT  22571  nmophmi  22607  leoprf2  22703  stlesi  22817  derangen  23110  subfacval3  23127  cvmseu  23214  cvmliftmolem2  23220  cvmliftlem7  23229  cvmliftlem15  23236  cvmlift2lem9a  23241  cvmlift2lem9  23249  cvmlift2lem10  23250  cvmlift2lem11  23251  cvmlift2lem12  23252  cvmlift3lem6  23262  cvmlift3lem8  23264  eupares  23306  eupap1  23307  fznatpl1  23499  brbtwn2  23943  axlowdimlem3  23982  axlowdimlem16  23995  axcontlem8  24009  eqfnung2  24529  prltub  24671  ubpar  24672  supaub  24684  geme2  24686  inttop2  24926  intopcoaconb  24951  intopcoaconc  24952  qusp  24953  prcnt  24962  cmptdst  24979  prdnei  24984  tcnvec  25101  aidm2  25161  dualalg  25193  idfisf  25252  idsubfun  25269  setiscat  25390  lppotos  25555  fness  25693  ssref  25694  fnetr  25697  reftr  25700  fnessref  25704  refssfne  25705  neibastop1  25719  neibastop2  25721  tailfb  25737  filnetlem3  25740  fzadd2  25855  sdclem2  25863  metf1o  25880  ismtyhmeolem  25939  ismtyres  25943  heibor1lem  25944  bfplem2  25958  bfp  25959  rrncmslem  25967  iccbnd  25975  icccmpALT  25976  rngogrphom  26013  rngoisoco  26024  keridl  26068  fzsplit1nn0  26244  icodiamlt  26316  irrapxlem3  26320  irrapxlem4  26321  pell1234qrdich  26357  pell1qr1  26367  pell14qrgap  26371  pellqrexplicit  26373  rmspecfund  26405  fzmaxdif  26479  acongeq  26481  jm2.23  26500  jm3.1  26524  lmhmlnmsplit  26596  dsmm0cl  26617  dsmmacl  26618  dsmmsubg  26620  dsmmlss  26621  uvcff  26651  frlmsplit2  26654  lindfrn  26702  f1lindf  26703  lindsss  26705  hbt  26745  dgrsub2  26750  proot1ex  26931  dvconstbi  26962  bnj1452  28361  lsmcv2  28498  lsatcv0  28500  lcvexchlem4  28506  lcvexchlem5  28507  l1cvpat  28523  lfl0f  28538  lfladdcl  28540  lflnegcl  28544  lkrlss  28564  eqlkr  28568  lkrlsp  28571  lkrlsp2  28572  lshpkrcl  28585  lkrin  28633  1cvrjat  28943  llni  28976  llnle  28986  lplni  29000  lplnle  29008  llncvrlpln2  29025  2atmat  29029  lvoli  29043  lplncvrlvol2  29083  elpaddri  29270  paddclN  29310  pclclN  29359  pclfinN  29368  0psubclN  29411  1psubclN  29412  atpsubclN  29413  pmapsubclN  29414  osumclN  29435  pexmidN  29437  pexmidlem6N  29443  lhp2lt  29469  lautcnv  29558  idlaut  29564  lautco  29565  idldil  29582  ldilcnv  29583  ldilco  29584  ltrncnv  29614  idltrn  29618  cdleme16d  29749  cdleme50laut  30015  cdleme50ldil  30016  cdleme50ltrn  30025  ltrnco  30187  dian0  30508  dia0eldmN  30509  dia1eldmN  30510  dialss  30515  diaintclN  30527  docaclN  30593  doca2N  30595  djajN  30606  dibintclN  30636  diblss  30639  dicvaddcl  30659  dicvscacl  30660  dicn0  30661  cdlemn11a  30676  dihord2cN  30690  dihord11b  30691  dihord6apre  30725  dihmeetlem1N  30759  dihglblem5apreN  30760  dihpN  30805  dihjatcclem4  30890  dochkr1  30947  islpoldN  30953  lcfrlem31  31042  mapdpglem18  31158  mapdheq2  31198  mapdheq4  31201  mapdh6aN  31204  hdmap1l6a  31279  hdmap1neglem1N  31297  hdmap14lem4a  31343
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator