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

Theorem mpbi2and 710
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 514 . 2 (𝜑 → (𝜓𝜒))
4 mpbi2and.3 . 2 (𝜑 → ((𝜓𝜒) ↔ 𝜃))
53, 4mpbid 234 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398
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 209  df-an 399
This theorem is referenced by:  supiso  8931  hartogslem1  8998  cantnfp1lem3  9135  oemapwe  9149  cantnffval2  9150  mulne0d  11284  flflp1  13169  flval2  13176  remim  14468  ntrivcvgtail  15248  divalgmod  15749  divnumden  16080  numdensq  16086  prmdivdiv  16116  4sqlem7  16272  isposd  17557  latasymd  17659  latjidm  17676  latmidm  17688  latledi  17691  latjass  17697  mod1ile  17707  isglbd  17719  lubun  17725  poslubmo  17748  posglbmo  17749  ismgmid2  17870  oppginv  18479  slwhash  18741  lsmmod  18793  iscmnd  18911  dprd2da  19156  dmdprdsplit2lem  19159  dprdsplit  19162  pgpfac1lem1  19188  imasring  19361  isdrngd  19519  subrg1  19537  lsmsp  19850  lspprabs  19859  lsmcv  19905  psr1  20184  mat1  21048  lmcn2  22249  dvdsq1p  24746  wilthlem2  25638  dchr1  25825  ismir  26437  vdgfrgrgt2  28069  atcvatlem  30154  ressprs  30635  rngurd  30850  ordtconnlem1  31155  cvmliftphtlem  32552  cvmlift3lem6  32559  cvmlift3lem9  32562  poimirlem13  34887  poimirlem14  34888  lsatexch  36161  lsatcvatlem  36167  oldmm1  36335  olj01  36343  olm01  36354  cvrcmp  36401  atcvreq0  36432  cvlexchb1  36448  cvlcvr1  36457  exatleN  36522  hlrelat3  36530  cvrval3  36531  cvratlem  36539  atlelt  36556  cvrat3  36560  2atjm  36563  atbtwn  36564  hlatexch3N  36598  hlatexch4  36599  2llnmat  36642  2atm  36645  lplnexllnN  36682  2llnjaN  36684  4atlem11b  36726  4atlem12b  36729  2lplnja  36737  dalem1  36777  dalemcea  36778  dalem3  36782  dalem8  36788  dalem16  36797  dalem17  36798  dalem21  36812  dalem25  36816  dalem39  36829  dalem54  36844  dalem55  36845  dalem57  36847  dalem60  36850  2lnat  36902  2atm2atN  36903  2llnma1b  36904  cdlema1N  36909  paddasslem12  36949  paddasslem13  36950  pmodlem1  36964  dalawlem2  36990  dalawlem3  36991  dalawlem5  36993  dalawlem6  36994  dalawlem8  36996  dalawlem11  36999  dalawlem12  37000  osumcllem1N  37074  lhp2lt  37119  lhpexle2lem  37127  lhpexle3lem  37129  lhpocnle  37134  lhpat3  37164  4atexlemtlw  37185  4atexlemnclw  37188  4atexlemcnd  37190  lautj  37211  lautm  37212  trlval3  37305  cdlemc5  37313  cdlemd3  37318  cdleme3g  37352  cdleme3h  37353  cdleme7d  37364  cdleme11c  37379  cdleme11k  37386  cdleme15d  37395  cdleme16e  37400  cdleme16f  37401  cdleme17b  37405  cdlemednpq  37417  cdleme19a  37421  cdleme20j  37436  cdleme21c  37445  cdleme22aa  37457  cdleme22b  37459  cdleme22cN  37460  cdleme22d  37461  cdleme23c  37469  cdleme28a  37488  cdleme35a  37566  cdleme35b  37568  cdleme35f  37572  cdleme42i  37601  cdlemeg46req  37647  cdlemf2  37680  cdlemg4c  37730  cdlemg6c  37738  cdlemg8b  37746  cdlemg10  37759  cdlemg11b  37760  cdlemg12f  37766  cdlemg13a  37769  cdlemg17a  37779  cdlemg17dALTN  37782  cdlemg18b  37797  cdlemg19a  37801  cdlemg27a  37810  cdlemg33b0  37819  cdlemg35  37831  cdlemg42  37847  cdlemg46  37853  trljco  37858  tendopltp  37898  cdlemi  37938  cdlemk3  37951  cdlemk10  37961  cdlemk15  37973  cdlemk1u  37977  cdlemk39  38034  cdlemk50  38070  erng1lem  38105  erngdvlem4  38109  erngdvlem4-rN  38117  dialss  38164  dia2dimlem1  38182  dia2dimlem10  38191  dia2dimlem12  38193  cdlemm10N  38236  djajN  38255  diblss  38288  cdlemn2  38313  dihjustlem  38334  dihord1  38336  dihord2pre2  38344  dib2dim  38361  dih2dimb  38362  dih2dimbALTN  38363  dihopelvalcpre  38366  dihord5b  38377  dihord5apre  38380  dihmeetlem1N  38408  dihglblem5apreN  38409  dihglblem2N  38412  dihmeetlem2N  38417  dihmeetlem3N  38423  lclkrlem2f  38630  lclkrlem2v  38646  lclkrslem2  38656  lcfrlem25  38685  lcfrlem35  38695  mapdlsm  38782  numdenexp  39166  fourierdlem54  42425  fourierdlem76  42447
  Copyright terms: Public domain W3C validator