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

Theorem mpbi2and 994
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 555 . 2 (𝜑 → (𝜓𝜒))
4 mpbi2and.3 . 2 (𝜑 → ((𝜓𝜒) ↔ 𝜃))
53, 4mpbid 222 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383
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 385
This theorem is referenced by:  supiso  8548  hartogslem1  8614  cantnfp1lem3  8752  oemapwe  8766  cantnffval2  8767  mulne0d  10891  flflp1  12822  flval2  12829  remim  14076  ntrivcvgtail  14851  divalgmod  15351  divalgmodOLD  15352  divnumden  15678  numdensq  15684  prmdivdiv  15714  4sqlem7  15870  isposd  17176  latasymd  17278  latjidm  17295  latmidm  17307  latledi  17310  latjass  17316  mod1ile  17326  isglbd  17338  lubun  17344  poslubmo  17367  posglbmo  17368  ismgmid2  17488  oppginv  18009  slwhash  18259  lsmmod  18308  iscmnd  18425  dprd2da  18661  dmdprdsplit2lem  18664  dprdsplit  18667  pgpfac1lem1  18693  imasring  18839  isdrngd  18994  subrg1  19012  lsmsp  19308  lspprabs  19317  lsmcv  19363  psr1  19634  mat1  20475  topgele  20956  lmcn2  21674  dvdsq1p  24139  wilthlem2  25015  dchr1  25202  ismir  25774  vdgfrgrgt2  27473  atcvatlem  29574  ressprs  29985  rngurd  30118  ordtconnlem1  30300  cvmliftphtlem  31627  cvmlift3lem6  31634  cvmlift3lem9  31637  poimirlem13  33753  poimirlem14  33754  lsatexch  34851  lsatcvatlem  34857  oldmm1  35025  olj01  35033  olm01  35044  cvrcmp  35091  atcvreq0  35122  cvlexchb1  35138  cvlcvr1  35147  exatleN  35211  hlrelat3  35219  cvrval3  35220  cvratlem  35228  atlelt  35245  cvrat3  35249  2atjm  35252  atbtwn  35253  hlatexch3N  35287  hlatexch4  35288  2llnmat  35331  2atm  35334  lplnexllnN  35371  2llnjaN  35373  4atlem11b  35415  4atlem12b  35418  2lplnja  35426  dalem1  35466  dalemcea  35467  dalem3  35471  dalem8  35477  dalem16  35486  dalem17  35487  dalem21  35501  dalem25  35505  dalem39  35518  dalem54  35533  dalem55  35534  dalem57  35536  dalem60  35539  2lnat  35591  2atm2atN  35592  2llnma1b  35593  cdlema1N  35598  paddasslem12  35638  paddasslem13  35639  pmodlem1  35653  dalawlem2  35679  dalawlem3  35680  dalawlem5  35682  dalawlem6  35683  dalawlem8  35685  dalawlem11  35688  dalawlem12  35689  osumcllem1N  35763  lhp2lt  35808  lhpexle2lem  35816  lhpexle3lem  35818  lhpocnle  35823  lhpat3  35853  4atexlemtlw  35874  4atexlemnclw  35877  4atexlemcnd  35879  lautj  35900  lautm  35901  trlval3  35995  cdlemc5  36003  cdlemd3  36008  cdleme3g  36042  cdleme3h  36043  cdleme7d  36054  cdleme11c  36069  cdleme11k  36076  cdleme15d  36085  cdleme16e  36090  cdleme16f  36091  cdleme17b  36095  cdlemednpq  36107  cdleme19a  36111  cdleme20j  36126  cdleme21c  36135  cdleme22aa  36147  cdleme22b  36149  cdleme22cN  36150  cdleme22d  36151  cdleme23c  36159  cdleme28a  36178  cdleme35a  36256  cdleme35b  36258  cdleme35f  36262  cdleme42i  36291  cdlemeg46req  36337  cdlemf2  36370  cdlemg4c  36420  cdlemg6c  36428  cdlemg8b  36436  cdlemg10  36449  cdlemg11b  36450  cdlemg12f  36456  cdlemg13a  36459  cdlemg17a  36469  cdlemg17dALTN  36472  cdlemg18b  36487  cdlemg19a  36491  cdlemg27a  36500  cdlemg33b0  36509  cdlemg35  36521  cdlemg42  36537  cdlemg46  36543  trljco  36548  tendopltp  36588  cdlemi  36628  cdlemk3  36641  cdlemk10  36651  cdlemk15  36663  cdlemk1u  36667  cdlemk39  36724  cdlemk50  36760  erng1lem  36795  erngdvlem4  36799  erngdvlem4-rN  36807  dialss  36855  dia2dimlem1  36873  dia2dimlem10  36882  dia2dimlem12  36884  cdlemm10N  36927  djajN  36946  diblss  36979  cdlemn2  37004  dihjustlem  37025  dihord1  37027  dihord2pre2  37035  dib2dim  37052  dih2dimb  37053  dih2dimbALTN  37054  dihopelvalcpre  37057  dihord5b  37068  dihord5apre  37071  dihmeetlem1N  37099  dihglblem5apreN  37100  dihglblem2N  37103  dihmeetlem2N  37108  dihmeetlem3N  37114  lclkrlem2f  37321  lclkrlem2v  37337  lclkrslem2  37347  lcfrlem25  37376  lcfrlem35  37386  mapdlsm  37473  fourierdlem54  40898  fourierdlem76  40920
  Copyright terms: Public domain W3C validator