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

Theorem mpbi2and 694
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 503 . 2 (𝜑 → (𝜓𝜒))
4 mpbi2and.3 . 2 (𝜑 → ((𝜓𝜒) ↔ 𝜃))
53, 4mpbid 223 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  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 198  df-an 385
This theorem is referenced by:  supiso  8630  hartogslem1  8696  cantnfp1lem3  8834  oemapwe  8848  cantnffval2  8849  mulne0d  10974  flflp1  12852  flval2  12859  remim  14100  ntrivcvgtail  14873  divalgmod  15369  divnumden  15693  numdensq  15699  prmdivdiv  15729  4sqlem7  15885  isposd  17180  latasymd  17282  latjidm  17299  latmidm  17311  latledi  17314  latjass  17320  mod1ile  17330  isglbd  17342  lubun  17348  poslubmo  17371  posglbmo  17372  ismgmid2  17492  oppginv  18010  slwhash  18260  lsmmod  18309  iscmnd  18426  dprd2da  18663  dmdprdsplit2lem  18666  dprdsplit  18669  pgpfac1lem1  18695  imasring  18841  isdrngd  18996  subrg1  19014  lsmsp  19313  lspprabs  19322  lsmcv  19369  psr1  19641  mat1  20485  topgele  20969  lmcn2  21687  dvdsq1p  24157  wilthlem2  25032  dchr1  25219  ismir  25791  vdgfrgrgt2  27496  atcvatlem  29595  ressprs  30003  rngurd  30136  ordtconnlem1  30318  cvmliftphtlem  31644  cvmlift3lem6  31651  cvmlift3lem9  31654  poimirlem13  33754  poimirlem14  33755  lsatexch  34842  lsatcvatlem  34848  oldmm1  35016  olj01  35024  olm01  35035  cvrcmp  35082  atcvreq0  35113  cvlexchb1  35129  cvlcvr1  35138  exatleN  35203  hlrelat3  35211  cvrval3  35212  cvratlem  35220  atlelt  35237  cvrat3  35241  2atjm  35244  atbtwn  35245  hlatexch3N  35279  hlatexch4  35280  2llnmat  35323  2atm  35326  lplnexllnN  35363  2llnjaN  35365  4atlem11b  35407  4atlem12b  35410  2lplnja  35418  dalem1  35458  dalemcea  35459  dalem3  35463  dalem8  35469  dalem16  35478  dalem17  35479  dalem21  35493  dalem25  35497  dalem39  35510  dalem54  35525  dalem55  35526  dalem57  35528  dalem60  35531  2lnat  35583  2atm2atN  35584  2llnma1b  35585  cdlema1N  35590  paddasslem12  35630  paddasslem13  35631  pmodlem1  35645  dalawlem2  35671  dalawlem3  35672  dalawlem5  35674  dalawlem6  35675  dalawlem8  35677  dalawlem11  35680  dalawlem12  35681  osumcllem1N  35755  lhp2lt  35800  lhpexle2lem  35808  lhpexle3lem  35810  lhpocnle  35815  lhpat3  35845  4atexlemtlw  35866  4atexlemnclw  35869  4atexlemcnd  35871  lautj  35892  lautm  35893  trlval3  35986  cdlemc5  35994  cdlemd3  35999  cdleme3g  36033  cdleme3h  36034  cdleme7d  36045  cdleme11c  36060  cdleme11k  36067  cdleme15d  36076  cdleme16e  36081  cdleme16f  36082  cdleme17b  36086  cdlemednpq  36098  cdleme19a  36102  cdleme20j  36117  cdleme21c  36126  cdleme22aa  36138  cdleme22b  36140  cdleme22cN  36141  cdleme22d  36142  cdleme23c  36150  cdleme28a  36169  cdleme35a  36247  cdleme35b  36249  cdleme35f  36253  cdleme42i  36282  cdlemeg46req  36328  cdlemf2  36361  cdlemg4c  36411  cdlemg6c  36419  cdlemg8b  36427  cdlemg10  36440  cdlemg11b  36441  cdlemg12f  36447  cdlemg13a  36450  cdlemg17a  36460  cdlemg17dALTN  36463  cdlemg18b  36478  cdlemg19a  36482  cdlemg27a  36491  cdlemg33b0  36500  cdlemg35  36512  cdlemg42  36528  cdlemg46  36534  trljco  36539  tendopltp  36579  cdlemi  36619  cdlemk3  36632  cdlemk10  36642  cdlemk15  36654  cdlemk1u  36658  cdlemk39  36715  cdlemk50  36751  erng1lem  36786  erngdvlem4  36790  erngdvlem4-rN  36798  dialss  36845  dia2dimlem1  36863  dia2dimlem10  36872  dia2dimlem12  36874  cdlemm10N  36917  djajN  36936  diblss  36969  cdlemn2  36994  dihjustlem  37015  dihord1  37017  dihord2pre2  37025  dib2dim  37042  dih2dimb  37043  dih2dimbALTN  37044  dihopelvalcpre  37047  dihord5b  37058  dihord5apre  37061  dihmeetlem1N  37089  dihglblem5apreN  37090  dihglblem2N  37093  dihmeetlem2N  37098  dihmeetlem3N  37104  lclkrlem2f  37311  lclkrlem2v  37327  lclkrslem2  37337  lcfrlem25  37366  lcfrlem35  37376  mapdlsm  37463  fourierdlem54  40874  fourierdlem76  40896
  Copyright terms: Public domain W3C validator