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

Theorem mpbi2and 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
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 519 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
4 mpbi2and.3 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  <->  th ) )
53, 4mpbid 202 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  supiso  7477  hartogslem1  7511  cantnfp1lem3  7636  oemapwe  7650  cantnffval2  7651  mulne0d  9674  flval2  11221  remim  11922  divalgmod  12926  divnumden  13140  numdensq  13146  prmdivdiv  13176  4sqlem7  13312  isposd  14412  latasymd  14486  latjidm  14503  latmidm  14515  latledi  14518  latjass  14524  mod1ile  14534  isglbd  14544  lubun  14550  poslubmo  14573  ismgmid2  14713  oppginv  15155  slwhash  15258  lsmmod  15307  iscmnd  15424  dprd2da  15600  dmdprdsplit2lem  15603  dprdsplit  15606  pgpfac1lem1  15632  imasrng  15725  isdrngd  15860  subrg1  15878  lsmsp  16158  lspprabs  16167  lsmcv  16213  psr1  16475  topgele  16999  lmcn2  17681  dvdsq1p  20083  wilthlem2  20852  dchr1  21041  atcvatlem  23888  cvmliftphtlem  25004  cvmlift3lem6  25011  cvmlift3lem9  25014  ntrivcvgtail  25228  lxflflp1  26241  mat1  27459  lubunNEW  29771  lsatexch  29841  lsatcvatlem  29847  oldmm1  30015  olj01  30023  olm01  30034  cvrcmp  30081  atcvreq0  30112  cvlexchb1  30128  cvlcvr1  30137  exatleN  30201  hlrelat3  30209  cvrval3  30210  cvratlem  30218  atlelt  30235  cvrat3  30239  2atjm  30242  atbtwn  30243  hlatexch3N  30277  hlatexch4  30278  2llnmat  30321  2atm  30324  lplnexllnN  30361  2llnjaN  30363  4atlem11b  30405  4atlem12b  30408  2lplnja  30416  dalem1  30456  dalemcea  30457  dalem3  30461  dalem8  30467  dalem16  30476  dalem17  30477  dalem21  30491  dalem25  30495  dalem39  30508  dalem54  30523  dalem55  30524  dalem57  30526  dalem60  30529  2lnat  30581  2atm2atN  30582  2llnma1b  30583  cdlema1N  30588  paddasslem12  30628  paddasslem13  30629  pmodlem1  30643  dalawlem2  30669  dalawlem3  30670  dalawlem5  30672  dalawlem6  30673  dalawlem8  30675  dalawlem11  30678  dalawlem12  30679  osumcllem1N  30753  lhp2lt  30798  lhpexle2lem  30806  lhpexle3lem  30808  lhpocnle  30813  lhpat3  30843  4atexlemtlw  30864  4atexlemnclw  30867  4atexlemcnd  30869  lautj  30890  lautm  30891  trlval3  30984  cdlemc5  30992  cdlemd3  30997  cdleme3g  31031  cdleme3h  31032  cdleme7d  31043  cdleme11c  31058  cdleme11k  31065  cdleme15d  31074  cdleme16e  31079  cdleme16f  31080  cdleme17b  31084  cdlemednpq  31096  cdleme19a  31100  cdleme20j  31115  cdleme21c  31124  cdleme22aa  31136  cdleme22b  31138  cdleme22cN  31139  cdleme22d  31140  cdleme23c  31148  cdleme28a  31167  cdleme35a  31245  cdleme35b  31247  cdleme35f  31251  cdleme42i  31280  cdlemeg46req  31326  cdlemf2  31359  cdlemg4c  31409  cdlemg6c  31417  cdlemg8b  31425  cdlemg10  31438  cdlemg11b  31439  cdlemg12f  31445  cdlemg13a  31448  cdlemg17a  31458  cdlemg17dALTN  31461  cdlemg18b  31476  cdlemg19a  31480  cdlemg27a  31489  cdlemg33b0  31498  cdlemg35  31510  cdlemg42  31526  cdlemg46  31532  trljco  31537  tendopltp  31577  cdlemi  31617  cdlemk3  31630  cdlemk10  31640  cdlemk15  31652  cdlemk1u  31656  cdlemk39  31713  cdlemk50  31749  erng1lem  31784  erngdvlem4  31788  erngdvlem4-rN  31796  dialss  31844  dia2dimlem1  31862  dia2dimlem10  31871  dia2dimlem12  31873  cdlemm10N  31916  djajN  31935  diblss  31968  cdlemn2  31993  dihjustlem  32014  dihord1  32016  dihord2pre2  32024  dib2dim  32041  dih2dimb  32042  dih2dimbALTN  32043  dihopelvalcpre  32046  dihord5b  32057  dihord5apre  32060  dihmeetlem1N  32088  dihglblem5apreN  32089  dihglblem2N  32092  dihmeetlem2N  32097  dihmeetlem3N  32103  lclkrlem2f  32310  lclkrlem2v  32326  lclkrslem2  32336  lcfrlem25  32365  lcfrlem35  32375  mapdlsm  32462
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 178  df-an 361
  Copyright terms: Public domain W3C validator