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

Theorem mpbi2and 955
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 554 . 2 (𝜑 → (𝜓𝜒))
4 mpbi2and.3 . 2 (𝜑 → ((𝜓𝜒) ↔ 𝜃))
53, 4mpbid 222 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384
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 197  df-an 386
This theorem is referenced by:  supiso  8366  hartogslem1  8432  cantnfp1lem3  8562  oemapwe  8576  cantnffval2  8577  mulne0d  10664  flflp1  12591  flval2  12598  remim  13838  ntrivcvgtail  14613  divalgmod  15110  divalgmodOLD  15111  divnumden  15437  numdensq  15443  prmdivdiv  15473  4sqlem7  15629  isposd  16936  latasymd  17038  latjidm  17055  latmidm  17067  latledi  17070  latjass  17076  mod1ile  17086  isglbd  17098  lubun  17104  poslubmo  17127  posglbmo  17128  ismgmid2  17248  oppginv  17770  slwhash  18020  lsmmod  18069  iscmnd  18186  dprd2da  18422  dmdprdsplit2lem  18425  dprdsplit  18428  pgpfac1lem1  18454  imasring  18600  isdrngd  18753  subrg1  18771  lsmsp  19067  lspprabs  19076  lsmcv  19122  psr1  19393  mat1  20234  topgele  20715  lmcn2  21433  dvdsq1p  23901  wilthlem2  24776  dchr1  24963  ismir  25535  vdgfrgrgt2  27142  atcvatlem  29214  ressprs  29629  rngurd  29762  ordtconnlem1  29944  cvmliftphtlem  31273  cvmlift3lem6  31280  cvmlift3lem9  31283  poimirlem13  33393  poimirlem14  33394  lsatexch  34149  lsatcvatlem  34155  oldmm1  34323  olj01  34331  olm01  34342  cvrcmp  34389  atcvreq0  34420  cvlexchb1  34436  cvlcvr1  34445  exatleN  34509  hlrelat3  34517  cvrval3  34518  cvratlem  34526  atlelt  34543  cvrat3  34547  2atjm  34550  atbtwn  34551  hlatexch3N  34585  hlatexch4  34586  2llnmat  34629  2atm  34632  lplnexllnN  34669  2llnjaN  34671  4atlem11b  34713  4atlem12b  34716  2lplnja  34724  dalem1  34764  dalemcea  34765  dalem3  34769  dalem8  34775  dalem16  34784  dalem17  34785  dalem21  34799  dalem25  34803  dalem39  34816  dalem54  34831  dalem55  34832  dalem57  34834  dalem60  34837  2lnat  34889  2atm2atN  34890  2llnma1b  34891  cdlema1N  34896  paddasslem12  34936  paddasslem13  34937  pmodlem1  34951  dalawlem2  34977  dalawlem3  34978  dalawlem5  34980  dalawlem6  34981  dalawlem8  34983  dalawlem11  34986  dalawlem12  34987  osumcllem1N  35061  lhp2lt  35106  lhpexle2lem  35114  lhpexle3lem  35116  lhpocnle  35121  lhpat3  35151  4atexlemtlw  35172  4atexlemnclw  35175  4atexlemcnd  35177  lautj  35198  lautm  35199  trlval3  35293  cdlemc5  35301  cdlemd3  35306  cdleme3g  35340  cdleme3h  35341  cdleme7d  35352  cdleme11c  35367  cdleme11k  35374  cdleme15d  35383  cdleme16e  35388  cdleme16f  35389  cdleme17b  35393  cdlemednpq  35405  cdleme19a  35410  cdleme20j  35425  cdleme21c  35434  cdleme22aa  35446  cdleme22b  35448  cdleme22cN  35449  cdleme22d  35450  cdleme23c  35458  cdleme28a  35477  cdleme35a  35555  cdleme35b  35557  cdleme35f  35561  cdleme42i  35590  cdlemeg46req  35636  cdlemf2  35669  cdlemg4c  35719  cdlemg6c  35727  cdlemg8b  35735  cdlemg10  35748  cdlemg11b  35749  cdlemg12f  35755  cdlemg13a  35758  cdlemg17a  35768  cdlemg17dALTN  35771  cdlemg18b  35786  cdlemg19a  35790  cdlemg27a  35799  cdlemg33b0  35808  cdlemg35  35820  cdlemg42  35836  cdlemg46  35842  trljco  35847  tendopltp  35887  cdlemi  35927  cdlemk3  35940  cdlemk10  35950  cdlemk15  35962  cdlemk1u  35966  cdlemk39  36023  cdlemk50  36059  erng1lem  36094  erngdvlem4  36098  erngdvlem4-rN  36106  dialss  36154  dia2dimlem1  36172  dia2dimlem10  36181  dia2dimlem12  36183  cdlemm10N  36226  djajN  36245  diblss  36278  cdlemn2  36303  dihjustlem  36324  dihord1  36326  dihord2pre2  36334  dib2dim  36351  dih2dimb  36352  dih2dimbALTN  36353  dihopelvalcpre  36356  dihord5b  36367  dihord5apre  36370  dihmeetlem1N  36398  dihglblem5apreN  36399  dihglblem2N  36402  dihmeetlem2N  36407  dihmeetlem3N  36413  lclkrlem2f  36620  lclkrlem2v  36636  lclkrslem2  36646  lcfrlem25  36675  lcfrlem35  36685  mapdlsm  36772  fourierdlem54  40140  fourierdlem76  40162
  Copyright terms: Public domain W3C validator