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

Theorem mpbi2and 708
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 512 . 2 (𝜑 → (𝜓𝜒))
4 mpbi2and.3 . 2 (𝜑 → ((𝜓𝜒) ↔ 𝜃))
53, 4mpbid 233 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  supiso  8928  hartogslem1  8995  cantnfp1lem3  9132  oemapwe  9146  cantnffval2  9147  mulne0d  11281  flflp1  13167  flval2  13174  remim  14466  ntrivcvgtail  15246  divalgmod  15747  divnumden  16078  numdensq  16084  prmdivdiv  16114  4sqlem7  16270  isposd  17555  latasymd  17657  latjidm  17674  latmidm  17686  latledi  17689  latjass  17695  mod1ile  17705  isglbd  17717  lubun  17723  poslubmo  17746  posglbmo  17747  ismgmid2  17868  oppginv  18427  slwhash  18680  lsmmod  18732  iscmnd  18850  dprd2da  19095  dmdprdsplit2lem  19098  dprdsplit  19101  pgpfac1lem1  19127  imasring  19300  isdrngd  19458  subrg1  19476  lsmsp  19789  lspprabs  19798  lsmcv  19844  psr1  20122  mat1  20986  lmcn2  22187  dvdsq1p  24683  wilthlem2  25574  dchr1  25761  ismir  26373  vdgfrgrgt2  28005  atcvatlem  30090  ressprs  30570  rngurd  30785  ordtconnlem1  31067  cvmliftphtlem  32462  cvmlift3lem6  32469  cvmlift3lem9  32472  poimirlem13  34787  poimirlem14  34788  lsatexch  36061  lsatcvatlem  36067  oldmm1  36235  olj01  36243  olm01  36254  cvrcmp  36301  atcvreq0  36332  cvlexchb1  36348  cvlcvr1  36357  exatleN  36422  hlrelat3  36430  cvrval3  36431  cvratlem  36439  atlelt  36456  cvrat3  36460  2atjm  36463  atbtwn  36464  hlatexch3N  36498  hlatexch4  36499  2llnmat  36542  2atm  36545  lplnexllnN  36582  2llnjaN  36584  4atlem11b  36626  4atlem12b  36629  2lplnja  36637  dalem1  36677  dalemcea  36678  dalem3  36682  dalem8  36688  dalem16  36697  dalem17  36698  dalem21  36712  dalem25  36716  dalem39  36729  dalem54  36744  dalem55  36745  dalem57  36747  dalem60  36750  2lnat  36802  2atm2atN  36803  2llnma1b  36804  cdlema1N  36809  paddasslem12  36849  paddasslem13  36850  pmodlem1  36864  dalawlem2  36890  dalawlem3  36891  dalawlem5  36893  dalawlem6  36894  dalawlem8  36896  dalawlem11  36899  dalawlem12  36900  osumcllem1N  36974  lhp2lt  37019  lhpexle2lem  37027  lhpexle3lem  37029  lhpocnle  37034  lhpat3  37064  4atexlemtlw  37085  4atexlemnclw  37088  4atexlemcnd  37090  lautj  37111  lautm  37112  trlval3  37205  cdlemc5  37213  cdlemd3  37218  cdleme3g  37252  cdleme3h  37253  cdleme7d  37264  cdleme11c  37279  cdleme11k  37286  cdleme15d  37295  cdleme16e  37300  cdleme16f  37301  cdleme17b  37305  cdlemednpq  37317  cdleme19a  37321  cdleme20j  37336  cdleme21c  37345  cdleme22aa  37357  cdleme22b  37359  cdleme22cN  37360  cdleme22d  37361  cdleme23c  37369  cdleme28a  37388  cdleme35a  37466  cdleme35b  37468  cdleme35f  37472  cdleme42i  37501  cdlemeg46req  37547  cdlemf2  37580  cdlemg4c  37630  cdlemg6c  37638  cdlemg8b  37646  cdlemg10  37659  cdlemg11b  37660  cdlemg12f  37666  cdlemg13a  37669  cdlemg17a  37679  cdlemg17dALTN  37682  cdlemg18b  37697  cdlemg19a  37701  cdlemg27a  37710  cdlemg33b0  37719  cdlemg35  37731  cdlemg42  37747  cdlemg46  37753  trljco  37758  tendopltp  37798  cdlemi  37838  cdlemk3  37851  cdlemk10  37861  cdlemk15  37873  cdlemk1u  37877  cdlemk39  37934  cdlemk50  37970  erng1lem  38005  erngdvlem4  38009  erngdvlem4-rN  38017  dialss  38064  dia2dimlem1  38082  dia2dimlem10  38091  dia2dimlem12  38093  cdlemm10N  38136  djajN  38155  diblss  38188  cdlemn2  38213  dihjustlem  38234  dihord1  38236  dihord2pre2  38244  dib2dim  38261  dih2dimb  38262  dih2dimbALTN  38263  dihopelvalcpre  38266  dihord5b  38277  dihord5apre  38280  dihmeetlem1N  38308  dihglblem5apreN  38309  dihglblem2N  38312  dihmeetlem2N  38317  dihmeetlem3N  38323  lclkrlem2f  38530  lclkrlem2v  38546  lclkrslem2  38556  lcfrlem25  38585  lcfrlem35  38595  mapdlsm  38682  numdenexp  39066  fourierdlem54  42326  fourierdlem76  42348
  Copyright terms: Public domain W3C validator