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:  fnpr  5850  fnprOLD  5851  dffi3  7331  supmax  7363  suppr  7366  ordtypelem7  7386  cantnfle  7519  cantnf0  7523  cantnfp1lem1  7527  cantnfp1lem2  7528  cantnfp1lem3  7529  oemapvali  7533  cantnflem1a  7534  cantnflem1c  7536  cantnflem1d  7537  cantnflem1  7538  cantnf  7542  mapfien  7546  rankpwi  7642  carduni  7761  fin23lem32  8117  fpwwe2lem6  8404  fpwwe2lem9  8407  fpwwe2lem12  8410  fpwwe2lem13  8411  fpwwe2  8412  inttsk  8543  grutsk1  8590  add20  9433  supmul  9869  suprzcl  10242  uzwo3  10462  rpnnen1lem5  10497  xrre  10650  xrre3  10652  xleadd1a  10725  xlemul1a  10760  supxrre  10799  infmxrre  10807  ixxub  10830  ixxlb  10831  elioc2  10866  elico2  10867  elicc2  10868  elfz1eq  10960  fzctr  11007  fzoaddel  11063  flid  11103  flval3  11109  fladdz  11114  fldiv  11128  modid  11157  seqf1olem1  11249  bcval5  11496  hashf1lem1  11591  sqeqd  11858  sqrlem7  11941  max0add  12002  abs2difabs  12025  rddif  12031  fzomaxdiflem  12033  rexico  12044  limsupgre  12162  rlim3  12179  icco1  12221  rlimclim  12227  rlimuni  12231  rlimresb  12246  isercolllem2  12346  isercolllem3  12347  isercoll  12348  caucvgrlem  12353  caurcvgr  12354  iseraltlem3  12364  fsum00  12464  o1fsum  12479  dvdseq  12784  bitsfzolem  12833  bitsfzo  12834  bitsmod  12835  bitscmp  12837  gcd0id  12910  gcdneg  12913  bezoutlem4  12928  nn0seqcvgd  12948  prmind2  12977  qredeq  12993  isprm5  12999  hashdvds  13051  eulerthlem2  13058  pcpremul  13104  pcidlem  13132  pcgcd1  13137  pcadd2  13146  fldivp1  13153  pcfaclem  13154  prmreclem5  13175  4sqlem17  13216  vdwlem1  13236  vdwlem6  13241  vdwlem12  13247  vdwlem13  13248  0ram  13275  ram0  13277  ramub1lem1  13281  invco  13883  sectmon  13890  monsect  13891  ssctr  13912  ssceq  13913  issubc3  13933  fullsubc  13934  funcinv  13957  fthmon  14011  fuccocl  14048  fucidcl  14049  invfuc  14058  elhomai  14075  setcmon  14129  setcepi  14130  catcisolem  14148  curf2cl  14215  yonedalem4c  14261  yonedalem3  14264  yoniso  14269  isacs3lem  14479  tsrdir  14570  nmznsg  14871  ghmpreima  14914  ghmeql  14915  ghmnsgpreima  14917  cntzsubm  15021  cntzsubg  15022  cntzmhm  15024  odlem2  15064  gexlem2  15103  gexcl2  15110  sylow1lem5  15123  subgslw  15137  slwhash  15145  fislw  15146  sylow3lem1  15148  lsmsubg  15175  efgredlemd  15263  efgredlem  15266  efgcpbllemb  15274  frgpuplem  15291  cyggeninv  15380  iscygd  15384  iscygodd  15385  gsumconst  15419  gsumpt  15432  dprdfcntz  15460  eldprdi  15463  subgdmdprd  15479  subgdprd  15480  dprdpr  15495  ablfac1c  15516  ablfac1eu  15518  ablfaclem3  15532  issubdrg  15780  rhmeql  15785  rhmima  15786  cntzsubr  15787  isabvd  15795  abvdiv  15812  lsslsp  15982  lmhmima  16014  lmhmpreima  16015  lmhmeql  16022  lsmcl  16046  lspfixed  16091  issubassa  16274  issubassa2  16294  psrbaglesupp  16324  psrbaglecl  16325  psrbagaddcl  16326  psrbagcon  16327  psrbas  16334  psrlidm  16358  psrridm  16359  mvridlem  16374  mplsubglem  16389  mpllsslem  16390  mplassa  16408  subrgmpl  16414  mplcoe3  16420  mplcoe2  16421  mplbas2  16422  mplind  16453  ply1assa  16488  coe1tmmul2  16562  coe1tmmul  16563  qsssubdrg  16648  gzrngunit  16654  ocvpj  16834  distop  16950  indistopon  16955  ppttop  16961  epttop  16963  mretopd  17046  toponmre  17047  neiss  17063  opnneissb  17068  ssnei2  17070  innei  17079  ordtcld1  17144  ordtcld2  17145  lmconst  17208  cnpnei  17210  iscncl  17215  cnss1  17222  cnss2  17223  cncnpi  17224  cncnp  17226  cnconst2  17228  cnrest  17230  cnpresti  17233  cnpdis  17238  paste  17239  lmcnp  17249  cnhaus  17299  hauscmp  17351  2ndcomap  17401  1stcelcls  17404  1stccnp  17405  llyrest  17428  nllyrest  17429  llyidm  17431  nllyidm  17432  kgentopon  17450  kgenidm  17459  kgencn3  17470  txcld  17515  tx1cn  17520  tx2cn  17521  ptcld  17524  xkoccn  17530  txcnp  17531  ptcnp  17533  txcnmpt  17535  ptcn  17538  txdis1cn  17546  ptrescn  17550  txkgen  17563  xkoco1cn  17568  xkoco2cn  17569  xkococn  17571  xkoinjcn  17598  qtoptop2  17607  qtopuni  17610  qtopid  17613  qtopkgen  17618  basqtop  17619  tgqtop  17620  qtopss  17623  qtopeu  17624  qtoprest  17625  kqopn  17642  kqcld  17643  kqreglem2  17650  reghmph  17701  ordthmeolem  17709  qtopf1  17724  opnfbas  17750  isfil2  17764  fbasweak  17773  fsubbas  17775  filcon  17791  fbasrn  17792  rnelfmlem  17860  flimss2  17880  flimss1  17881  hausflim  17889  flimclslem  17892  flimsncls  17894  cnpflfi  17907  flfcnp2  17915  fclsfnflim  17935  symgtgp  17997  opnsubg  18003  ghmcnp  18010  divstgpopn  18015  divstgplem  18016  divstgphaus  18018  tsmsfbas  18023  isxmetd  18104  xmetsym  18125  imasdsf1olem  18150  imasf1oxmet  18152  xblss2  18171  xblcntr  18176  blcld  18264  ngptgp  18365  tngngpd  18382  tngnrg  18398  nlmvscn  18411  nrginvrcn  18415  nmo0  18457  nmoeq0  18458  nmoid  18464  nghmcn  18467  0nmhm  18477  blcvx  18517  zcld  18532  iccntr  18540  xrge0tsms  18553  xmetdcn2  18556  metdstri  18569  metdscn  18574  rescncf  18615  cncfco  18625  oprpiece1res2  18665  cnheibor  18668  cnllycmp  18669  bndth  18671  evth  18672  ishtpyd  18688  isphtpyd  18699  pcoval2  18729  nmhmcn  18816  ipcn  18888  lmnn  18904  cfilss  18911  iscfil3  18914  cfilfcls  18915  cmetcaulem  18929  iscmet3lem2  18933  cfilres  18937  lmcau  18953  flimcfil  18954  cncmet  18959  rlmbn  18993  minveclem3b  19007  pjthlem1  19016  pjth2  19019  ivthlem3  19028  ovolssnul  19061  ovolctb  19064  ovolunnul  19074  ovoliunnul  19081  ovolsca  19089  ovolicc  19097  ovolicopnf  19098  voliunlem2  19123  voliunlem3  19124  volsup  19128  uniioovol  19149  uniiccvol  19150  dyadmaxlem  19167  vitalilem5  19182  ismbfd  19210  mbfres  19214  mbfss  19216  mbfmulc2re  19218  mbfadd  19231  mbfmulc2  19233  mbflimsup  19236  mbflim  19238  i1faddlem  19263  i1fmullem  19264  mbfmul  19296  itg2itg1  19306  itg2seq  19312  itg2eqa  19315  itg2mulc  19317  itg2split  19319  itg2mono  19323  itg2cnlem1  19331  ibl0  19356  iblposlem  19361  itgreval  19366  iblneg  19372  iblss  19374  iblss2  19375  itgle  19379  iblconst  19387  iblabs  19398  iblabsr  19399  iblmulc2  19400  bddmulibl  19408  limciun  19459  limcun  19460  dvres2lem  19475  dvidlem  19480  dvcnp2  19484  dvcn  19485  cpnres  19501  dvaddbr  19502  dvmulbr  19503  dvcobr  19510  dvcjbr  19513  dvrec  19519  dvcnvlem  19538  dvferm  19550  dvlip2  19557  dveq0  19562  dv11cn  19563  dvivthlem1  19570  lhop1  19576  lhop2  19577  lhop  19578  dvcnvre  19581  dvfsumlem3  19590  dvfsumlem4  19591  dvfsumrlim  19593  dvfsum2  19596  ftc1a  19599  ftc1lem4  19601  ftc1lem6  19603  ftc1  19604  evlslem3  19613  mpfind  19643  coe1mul3  19700  deg1addle2  19703  deg1add  19704  deg1sublt  19711  deg1mul2  19715  deg1tm  19719  fta1blem  19769  drnguc1p  19771  ig1prsp  19778  plyco0  19789  plyeq0lem  19807  dgrub  19831  dgreq  19841  dgradd2  19864  dgrmul  19866  dgrcolem2  19870  dgrco  19871  plycpn  19884  plydivlem4  19891  plydiveu  19893  vieta1lem2  19906  vieta1  19907  aalioulem2  19928  aalioulem3  19929  aaliou3lem7  19944  tayl0  19956  ulmcn  19993  ulmdvlem3  19996  psercn  20020  abelth  20035  pilem3  20047  efif1olem1  20122  abslogimle  20149  argregt0  20183  argrege0  20184  logf1o2  20219  cxpsqrlem  20271  cxpcn3  20310  abscxpbnd  20315  ang180lem2  20330  ang180lem3  20331  logreclem  20338  xrlimcnp  20485  harmonicbnd4  20527  fsumharmonic  20528  basellem3  20543  basellem4  20544  dvdsppwf1o  20649  dvdsflf1o  20650  fsumfldivdiaglem  20652  chpeq0  20670  chteq0  20671  chtub  20674  chpub  20682  dchrelbasd  20701  dchrmulcl  20711  dchrinv  20723  bcmono  20739  bposlem1  20746  bposlem2  20747  lgslem1  20758  lgsdirprm  20791  lgsqrlem2  20804  lgsqrlem3  20805  lgsdchr  20810  lgseisenlem1  20811  lgseisenlem2  20812  lgseisenlem3  20813  lgsquadlem1  20816  2sqlem8  20834  2sqblem  20839  chebbnd1lem1  20841  dchrisumlem1  20861  dchrisumlem2  20862  dchrisumlem3  20863  dchrisum0fno1  20883  pntrmax  20936  pntpbnd1a  20957  pntibndlem3  20964  pntlemn  20972  pntlemi  20976  pntlem3  20981  pntleml  20983  ostth1  21005  ostth2  21009  ostth3  21010  cusgra0v  21139  cusgraexi  21147  cusgrares  21151  eupares  21208  eupap1  21209  nvabs  21673  vacn  21701  nmcvcn  21702  nmblore  21798  0lno  21802  0blo  21804  nmlno0lem  21805  occl  22317  pjhthlem1  22404  pjpjpre  22432  nmopre  22884  nmlnop0iALT  23009  nmophmi  23045  leoprf2  23141  stlesi  23255  xrre3FL  23642  xrge0tsmsd  23735  mbfmcst  24193  imambfm  24196  mbfmco  24198  0rrv  24278  lgamgulmlem5  24386  lgambdd  24390  derangen  24427  subfacval3  24444  cvmseu  24531  cvmliftmolem2  24537  cvmliftlem7  24546  cvmliftlem15  24553  cvmlift2lem9a  24558  cvmlift2lem9  24566  cvmlift2lem10  24567  cvmlift2lem11  24568  cvmlift2lem12  24569  cvmlift3lem6  24579  cvmlift3lem8  24581  fznatpl1  24767  brbtwn2  25360  axlowdimlem3  25399  axlowdimlem16  25412  axcontlem8  25426  supaddc  25750  supadd  25751  ovoliunnfl  25756  volsupnfl  25759  itg2addnclem2  25761  iblabsnc  25772  iblmulc2nc  25773  ftc1cnnclem  25781  ftc1cnnc  25782  fness  25874  ssref  25875  fnetr  25878  reftr  25881  fnessref  25885  refssfne  25886  neibastop1  25900  neibastop2  25902  tailfb  25918  filnetlem3  25921  fzadd2  26036  sdclem2  26044  metf1o  26061  ismtyhmeolem  26119  ismtyres  26123  heibor1lem  26124  bfplem2  26138  bfp  26139  rrncmslem  26147  iccbnd  26155  icccmpALT  26156  rngogrphom  26193  rngoisoco  26204  keridl  26248  fzsplit1nn0  26424  icodiamlt  26496  irrapxlem3  26500  irrapxlem4  26501  pell1234qrdich  26537  pell1qr1  26547  pell14qrgap  26551  pellqrexplicit  26553  rmspecfund  26585  fzmaxdif  26659  acongeq  26661  jm2.23  26680  jm3.1  26704  lmhmlnmsplit  26776  dsmm0cl  26797  dsmmacl  26798  dsmmsubg  26800  dsmmlss  26801  uvcff  26831  frlmsplit2  26834  lindfrn  26882  f1lindf  26883  lindsss  26885  hbt  26925  dgrsub2  26930  proot1ex  27111  dvconstbi  27142  1pthon  27738  2pthon  27749  constr3trllem3  27787  constr3cycl  27796  frgra0v  27817  frgra1v  27822  bnj1452  28834  lsmcv2  29278  lsatcv0  29280  lcvexchlem4  29286  lcvexchlem5  29287  l1cvpat  29303  lfl0f  29318  lfladdcl  29320  lflnegcl  29324  lkrlss  29344  eqlkr  29348  lkrlsp  29351  lkrlsp2  29352  lshpkrcl  29365  lkrin  29413  1cvrjat  29723  llni  29756  llnle  29766  lplni  29780  lplnle  29788  llncvrlpln2  29805  2atmat  29809  lvoli  29823  lplncvrlvol2  29863  elpaddri  30050  paddclN  30090  pclclN  30139  pclfinN  30148  0psubclN  30191  1psubclN  30192  atpsubclN  30193  pmapsubclN  30194  osumclN  30215  pexmidN  30217  pexmidlem6N  30223  lhp2lt  30249  lautcnv  30338  idlaut  30344  lautco  30345  idldil  30362  ldilcnv  30363  ldilco  30364  ltrncnv  30394  idltrn  30398  cdleme16d  30529  cdleme50laut  30795  cdleme50ldil  30796  cdleme50ltrn  30805  ltrnco  30967  dian0  31288  dia0eldmN  31289  dia1eldmN  31290  dialss  31295  diaintclN  31307  docaclN  31373  doca2N  31375  djajN  31386  dibintclN  31416  diblss  31419  dicvaddcl  31439  dicvscacl  31440  dicn0  31441  cdlemn11a  31456  dihord2cN  31470  dihord11b  31471  dihord6apre  31505  dihmeetlem1N  31539  dihglblem5apreN  31540  dihpN  31585  dihjatcclem4  31670  dochkr1  31727  islpoldN  31733  lcfrlem31  31822  mapdpglem18  31938  mapdheq2  31978  mapdheq4  31981  mapdh6aN  31984  hdmap1l6a  32059  hdmap1neglem1N  32077  hdmap14lem4a  32123
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