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  7268  hartogslem1  7302  cantnfp1lem3  7427  oemapwe  7441  cantnffval2  7442  mulne0d  9465  lbinfm  9752  flval2  10991  remim  11649  divalgmod  12652  divnumden  12866  numdensq  12872  prmdivdiv  12902  4sqlem7  13038  isposd  14138  latasymd  14212  latjidm  14229  latmidm  14241  latledi  14244  latjass  14250  mod1ile  14260  isglbd  14270  lubun  14276  poslubmo  14299  ismgmid2  14439  oppginv  14881  slwhash  14984  lsmmod  15033  iscmnd  15150  dprd2da  15326  dmdprdsplit2lem  15329  dprdsplit  15332  pgpfac1lem1  15358  imasrng  15451  isdrngd  15586  subrg1  15604  lsmsp  15888  lspprabs  15897  lsmcv  15943  psr1  16205  topgele  16728  lmcn2  17399  dvdsq1p  19599  wilthlem2  20360  dchr1  20549  atcvatlem  23020  cvmliftphtlem  24132  cvmlift3lem6  24139  cvmlift3lem9  24142  ntrivcvgtail  24405  lxflflp1  25314  mat1  26630  lubunNEW  28981  lsatexch  29051  lsatcvatlem  29057  oldmm1  29225  olj01  29233  olm01  29244  cvrcmp  29291  atcvreq0  29322  cvlexchb1  29338  cvlcvr1  29347  exatleN  29411  hlrelat3  29419  cvrval3  29420  cvratlem  29428  atlelt  29445  cvrat3  29449  2atjm  29452  atbtwn  29453  hlatexch3N  29487  hlatexch4  29488  2llnmat  29531  2atm  29534  lplnexllnN  29571  2llnjaN  29573  4atlem11b  29615  4atlem12b  29618  2lplnja  29626  dalem1  29666  dalemcea  29667  dalem3  29671  dalem8  29677  dalem16  29686  dalem17  29687  dalem21  29701  dalem25  29705  dalem39  29718  dalem54  29733  dalem55  29734  dalem57  29736  dalem60  29739  2lnat  29791  2atm2atN  29792  2llnma1b  29793  cdlema1N  29798  paddasslem12  29838  paddasslem13  29839  pmodlem1  29853  dalawlem2  29879  dalawlem3  29880  dalawlem5  29882  dalawlem6  29883  dalawlem8  29885  dalawlem11  29888  dalawlem12  29889  osumcllem1N  29963  lhp2lt  30008  lhpexle2lem  30016  lhpexle3lem  30018  lhpocnle  30023  lhpat3  30053  4atexlemtlw  30074  4atexlemnclw  30077  4atexlemcnd  30079  lautj  30100  lautm  30101  trlval3  30194  cdlemc5  30202  cdlemd3  30207  cdleme3g  30241  cdleme3h  30242  cdleme7d  30253  cdleme11c  30268  cdleme11k  30275  cdleme15d  30284  cdleme16e  30289  cdleme16f  30290  cdleme17b  30294  cdlemednpq  30306  cdleme19a  30310  cdleme20j  30325  cdleme21c  30334  cdleme22aa  30346  cdleme22b  30348  cdleme22cN  30349  cdleme22d  30350  cdleme23c  30358  cdleme28a  30377  cdleme35a  30455  cdleme35b  30457  cdleme35f  30461  cdleme42i  30490  cdlemeg46req  30536  cdlemf2  30569  cdlemg4c  30619  cdlemg6c  30627  cdlemg8b  30635  cdlemg10  30648  cdlemg11b  30649  cdlemg12f  30655  cdlemg13a  30658  cdlemg17a  30668  cdlemg17dALTN  30671  cdlemg18b  30686  cdlemg19a  30690  cdlemg27a  30699  cdlemg33b0  30708  cdlemg35  30720  cdlemg42  30736  cdlemg46  30742  trljco  30747  tendopltp  30787  cdlemi  30827  cdlemk3  30840  cdlemk10  30850  cdlemk15  30862  cdlemk1u  30866  cdlemk39  30923  cdlemk50  30959  erng1lem  30994  erngdvlem4  30998  erngdvlem4-rN  31006  dialss  31054  dia2dimlem1  31072  dia2dimlem10  31081  dia2dimlem12  31083  cdlemm10N  31126  djajN  31145  diblss  31178  cdlemn2  31203  dihjustlem  31224  dihord1  31226  dihord2pre2  31234  dib2dim  31251  dih2dimb  31252  dih2dimbALTN  31253  dihopelvalcpre  31256  dihord5b  31267  dihord5apre  31270  dihmeetlem1N  31298  dihglblem5apreN  31299  dihglblem2N  31302  dihmeetlem2N  31307  dihmeetlem3N  31313  lclkrlem2f  31520  lclkrlem2v  31536  lclkrslem2  31546  lcfrlem25  31575  lcfrlem35  31585  mapdlsm  31672
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