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

Theorem mpbi2and 921
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
mpbi2and.2
mpbi2and.3
Assertion
Ref Expression
mpbi2and

Proof of Theorem mpbi2and
StepHypRef Expression
1 mpbi2and.1 . . 3
2 mpbi2and.2 . . 3
31, 2jca 532 . 2
4 mpbi2and.3 . 2
53, 4mpbid 210 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  supiso  7954  hartogslem1  7988  cantnfp1lem3  8120  oemapwe  8134  cantnffval2  8135  cantnfp1lem3OLD  8146  oemapweOLD  8156  cantnffval2OLD  8157  mulne0d  10226  flflp1  11944  flval2  11950  remim  12950  ntrivcvgtail  13709  divalgmod  14064  divnumden  14281  numdensq  14287  prmdivdiv  14317  4sqlem7  14462  isposd  15585  latasymd  15687  latjidm  15704  latmidm  15716  latledi  15719  latjass  15725  mod1ile  15735  isglbd  15747  lubun  15753  poslubmo  15776  posglbmo  15777  ismgmid2  15894  oppginv  16394  slwhash  16644  lsmmod  16693  iscmnd  16810  dprd2da  17091  dmdprdsplit2lem  17094  dprdsplit  17097  pgpfac1lem1  17125  imasring  17268  isdrngd  17421  subrg1  17439  lsmsp  17732  lspprabs  17741  lsmcv  17787  psr1  18067  mat1  18949  topgele  19435  lmcn2  20150  dvdsq1p  22561  wilthlem2  23343  dchr1  23532  ismir  24040  atcvatlem  27304  ressprs  27643  rngurd  27778  ordtconlem1  27906  cvmliftphtlem  28762  cvmlift3lem6  28769  cvmlift3lem9  28772  fourierdlem54  31943  fourierdlem76  31965  lsatexch  34768  lsatcvatlem  34774  oldmm1  34942  olj01  34950  olm01  34961  cvrcmp  35008  atcvreq0  35039  cvlexchb1  35055  cvlcvr1  35064  exatleN  35128  hlrelat3  35136  cvrval3  35137  cvratlem  35145  atlelt  35162  cvrat3  35166  2atjm  35169  atbtwn  35170  hlatexch3N  35204  hlatexch4  35205  2llnmat  35248  2atm  35251  lplnexllnN  35288  2llnjaN  35290  4atlem11b  35332  4atlem12b  35335  2lplnja  35343  dalem1  35383  dalemcea  35384  dalem3  35388  dalem8  35394  dalem16  35403  dalem17  35404  dalem21  35418  dalem25  35422  dalem39  35435  dalem54  35450  dalem55  35451  dalem57  35453  dalem60  35456  2lnat  35508  2atm2atN  35509  2llnma1b  35510  cdlema1N  35515  paddasslem12  35555  paddasslem13  35556  pmodlem1  35570  dalawlem2  35596  dalawlem3  35597  dalawlem5  35599  dalawlem6  35600  dalawlem8  35602  dalawlem11  35605  dalawlem12  35606  osumcllem1N  35680  lhp2lt  35725  lhpexle2lem  35733  lhpexle3lem  35735  lhpocnle  35740  lhpat3  35770  4atexlemtlw  35791  4atexlemnclw  35794  4atexlemcnd  35796  lautj  35817  lautm  35818  trlval3  35912  cdlemc5  35920  cdlemd3  35925  cdleme3g  35959  cdleme3h  35960  cdleme7d  35971  cdleme11c  35986  cdleme11k  35993  cdleme15d  36002  cdleme16e  36007  cdleme16f  36008  cdleme17b  36012  cdlemednpq  36024  cdleme19a  36029  cdleme20j  36044  cdleme21c  36053  cdleme22aa  36065  cdleme22b  36067  cdleme22cN  36068  cdleme22d  36069  cdleme23c  36077  cdleme28a  36096  cdleme35a  36174  cdleme35b  36176  cdleme35f  36180  cdleme42i  36209  cdlemeg46req  36255  cdlemf2  36288  cdlemg4c  36338  cdlemg6c  36346  cdlemg8b  36354  cdlemg10  36367  cdlemg11b  36368  cdlemg12f  36374  cdlemg13a  36377  cdlemg17a  36387  cdlemg17dALTN  36390  cdlemg18b  36405  cdlemg19a  36409  cdlemg27a  36418  cdlemg33b0  36427  cdlemg35  36439  cdlemg42  36455  cdlemg46  36461  trljco  36466  tendopltp  36506  cdlemi  36546  cdlemk3  36559  cdlemk10  36569  cdlemk15  36581  cdlemk1u  36585  cdlemk39  36642  cdlemk50  36678  erng1lem  36713  erngdvlem4  36717  erngdvlem4-rN  36725  dialss  36773  dia2dimlem1  36791  dia2dimlem10  36800  dia2dimlem12  36802  cdlemm10N  36845  djajN  36864  diblss  36897  cdlemn2  36922  dihjustlem  36943  dihord1  36945  dihord2pre2  36953  dib2dim  36970  dih2dimb  36971  dih2dimbALTN  36972  dihopelvalcpre  36975  dihord5b  36986  dihord5apre  36989  dihmeetlem1N  37017  dihglblem5apreN  37018  dihglblem2N  37021  dihmeetlem2N  37026  dihmeetlem3N  37032  lclkrlem2f  37239  lclkrlem2v  37255  lclkrslem2  37265  lcfrlem25  37294  lcfrlem35  37304  mapdlsm  37391
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator