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

Theorem mpbi2and 887
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
mpbi2and.1  |-  ( ph  ->  ps )
mpbi2and.2  |-  ( ph  ->  ch )
mpbi2and.3  |-  ( ph  ->  ( ( ps  /\  ch )  <->  th ) )
Assertion
Ref Expression
mpbi2and  |-  ( ph  ->  th )

Proof of Theorem mpbi2and
StepHypRef Expression
1 mpbi2and.1 . . 3  |-  ( ph  ->  ps )
2 mpbi2and.2 . . 3  |-  ( ph  ->  ch )
31, 2jca 518 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
4 mpbi2and.3 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  <->  th ) )
53, 4mpbid 201 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  supiso  7223  hartogslem1  7257  cantnfp1lem3  7382  oemapwe  7396  cantnffval2  7397  mulne0d  9420  lbinfm  9707  flval2  10944  remim  11602  divalgmod  12605  divnumden  12819  numdensq  12825  prmdivdiv  12855  4sqlem7  12991  isposd  14089  latasymd  14163  latjidm  14180  latmidm  14192  latledi  14195  latjass  14201  mod1ile  14211  isglbd  14221  lubun  14227  poslubmo  14250  ismgmid2  14390  oppginv  14832  slwhash  14935  lsmmod  14984  iscmnd  15101  dprd2da  15277  dmdprdsplit2lem  15280  dprdsplit  15283  pgpfac1lem1  15309  imasrng  15402  isdrngd  15537  subrg1  15555  lsmsp  15839  lspprabs  15848  lsmcv  15894  psr1  16156  topgele  16672  lmcn2  17343  dvdsq1p  19546  wilthlem2  20307  dchr1  20496  atcvatlem  22965  cvmliftphtlem  23848  cvmlift3lem6  23855  cvmlift3lem9  23858  pgapspf2  26053  lineval42  26080  mat1  27482  lubunNEW  29163  lsatexch  29233  lsatcvatlem  29239  oldmm1  29407  olj01  29415  olm01  29426  cvrcmp  29473  atcvreq0  29504  cvlexchb1  29520  cvlcvr1  29529  exatleN  29593  hlrelat3  29601  cvrval3  29602  cvratlem  29610  atlelt  29627  cvrat3  29631  2atjm  29634  atbtwn  29635  hlatexch3N  29669  hlatexch4  29670  2llnmat  29713  2atm  29716  lplnexllnN  29753  2llnjaN  29755  4atlem11b  29797  4atlem12b  29800  2lplnja  29808  dalem1  29848  dalemcea  29849  dalem3  29853  dalem8  29859  dalem16  29868  dalem17  29869  dalem21  29883  dalem25  29887  dalem39  29900  dalem54  29915  dalem55  29916  dalem57  29918  dalem60  29921  2lnat  29973  2atm2atN  29974  2llnma1b  29975  cdlema1N  29980  paddasslem12  30020  paddasslem13  30021  pmodlem1  30035  dalawlem2  30061  dalawlem3  30062  dalawlem5  30064  dalawlem6  30065  dalawlem8  30067  dalawlem11  30070  dalawlem12  30071  osumcllem1N  30145  lhp2lt  30190  lhpexle2lem  30198  lhpexle3lem  30200  lhpocnle  30205  lhpat3  30235  4atexlemtlw  30256  4atexlemnclw  30259  4atexlemcnd  30261  lautj  30282  lautm  30283  trlval3  30376  cdlemc5  30384  cdlemd3  30389  cdleme3g  30423  cdleme3h  30424  cdleme7d  30435  cdleme11c  30450  cdleme11k  30457  cdleme15d  30466  cdleme16e  30471  cdleme16f  30472  cdleme17b  30476  cdlemednpq  30488  cdleme19a  30492  cdleme20j  30507  cdleme21c  30516  cdleme22aa  30528  cdleme22b  30530  cdleme22cN  30531  cdleme22d  30532  cdleme23c  30540  cdleme28a  30559  cdleme35a  30637  cdleme35b  30639  cdleme35f  30643  cdleme42i  30672  cdlemeg46req  30718  cdlemf2  30751  cdlemg4c  30801  cdlemg6c  30809  cdlemg8b  30817  cdlemg10  30830  cdlemg11b  30831  cdlemg12f  30837  cdlemg13a  30840  cdlemg17a  30850  cdlemg17dALTN  30853  cdlemg18b  30868  cdlemg19a  30872  cdlemg27a  30881  cdlemg33b0  30890  cdlemg35  30902  cdlemg42  30918  cdlemg46  30924  trljco  30929  tendopltp  30969  cdlemi  31009  cdlemk3  31022  cdlemk10  31032  cdlemk15  31044  cdlemk1u  31048  cdlemk39  31105  cdlemk50  31141  erng1lem  31176  erngdvlem4  31180  erngdvlem4-rN  31188  dialss  31236  dia2dimlem1  31254  dia2dimlem10  31263  dia2dimlem12  31265  cdlemm10N  31308  djajN  31327  diblss  31360  cdlemn2  31385  dihjustlem  31406  dihord1  31408  dihord2pre2  31416  dib2dim  31433  dih2dimb  31434  dih2dimbALTN  31435  dihopelvalcpre  31438  dihord5b  31449  dihord5apre  31452  dihmeetlem1N  31480  dihglblem5apreN  31481  dihglblem2N  31484  dihmeetlem2N  31489  dihmeetlem3N  31495  lclkrlem2f  31702  lclkrlem2v  31718  lclkrslem2  31728  lcfrlem25  31757  lcfrlem35  31767  mapdlsm  31854
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