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

Theorem mpbi2and 711
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 513 . 2 (𝜑 → (𝜓𝜒))
4 mpbi2and.3 . 2 (𝜑 → ((𝜓𝜒) ↔ 𝜃))
53, 4mpbid 231 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397
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 206  df-an 398
This theorem is referenced by:  supiso  9416  hartogslem1  9483  cantnfp1lem3  9621  oemapwe  9635  cantnffval2  9636  mulne0d  11812  flflp1  13718  flval2  13725  remim  15008  ntrivcvgtail  15790  divalgmod  16293  divnumden  16628  numdensq  16634  prmdivdiv  16664  4sqlem7  16821  isposd  18217  poslubmo  18305  posglbmo  18306  latasymd  18339  latjidm  18356  latmidm  18368  latledi  18371  latjass  18377  mod1ile  18387  isglbd  18403  lubun  18409  ismgmid2  18528  oppginv  19145  slwhash  19411  lsmmod  19462  iscmnd  19581  dprd2da  19826  dmdprdsplit2lem  19829  dprdsplit  19832  pgpfac1lem1  19858  imasring  20050  isdrngd  20226  isdrngdOLD  20228  subrg1  20246  lsmsp  20562  lspprabs  20571  lsmcv  20618  psr1  21397  mat1  21812  lmcn2  23016  dvdsq1p  25541  wilthlem2  26434  dchr1  26621  ismir  27643  vdgfrgrgt2  29284  atcvatlem  31369  ressprs  31872  rngurd  32114  zarclssn  32511  ordtconnlem1  32562  cvmliftphtlem  33968  cvmlift3lem6  33975  cvmlift3lem9  33978  poimirlem13  36137  poimirlem14  36138  lsatexch  37551  lsatcvatlem  37557  oldmm1  37725  olj01  37733  olm01  37744  cvrcmp  37791  atcvreq0  37822  cvlexchb1  37838  cvlcvr1  37847  exatleN  37913  hlrelat3  37921  cvrval3  37922  cvratlem  37930  atlelt  37947  cvrat3  37951  2atjm  37954  atbtwn  37955  hlatexch3N  37989  hlatexch4  37990  2llnmat  38033  2atm  38036  lplnexllnN  38073  2llnjaN  38075  4atlem11b  38117  4atlem12b  38120  2lplnja  38128  dalem1  38168  dalemcea  38169  dalem3  38173  dalem8  38179  dalem16  38188  dalem17  38189  dalem21  38203  dalem25  38207  dalem39  38220  dalem54  38235  dalem55  38236  dalem57  38238  dalem60  38241  2lnat  38293  2atm2atN  38294  2llnma1b  38295  cdlema1N  38300  paddasslem12  38340  paddasslem13  38341  pmodlem1  38355  dalawlem2  38381  dalawlem3  38382  dalawlem5  38384  dalawlem6  38385  dalawlem8  38387  dalawlem11  38390  dalawlem12  38391  osumcllem1N  38465  lhp2lt  38510  lhpexle2lem  38518  lhpexle3lem  38520  lhpocnle  38525  lhpat3  38555  4atexlemtlw  38576  4atexlemnclw  38579  4atexlemcnd  38581  lautj  38602  lautm  38603  trlval3  38696  cdlemc5  38704  cdlemd3  38709  cdleme3g  38743  cdleme3h  38744  cdleme7d  38755  cdleme11c  38770  cdleme11k  38777  cdleme15d  38786  cdleme16e  38791  cdleme16f  38792  cdleme17b  38796  cdlemednpq  38808  cdleme19a  38812  cdleme20j  38827  cdleme21c  38836  cdleme22aa  38848  cdleme22b  38850  cdleme22cN  38851  cdleme22d  38852  cdleme23c  38860  cdleme28a  38879  cdleme35a  38957  cdleme35b  38959  cdleme35f  38963  cdleme42i  38992  cdlemeg46req  39038  cdlemf2  39071  cdlemg4c  39121  cdlemg6c  39129  cdlemg8b  39137  cdlemg10  39150  cdlemg11b  39151  cdlemg12f  39157  cdlemg13a  39160  cdlemg17a  39170  cdlemg17dALTN  39173  cdlemg18b  39188  cdlemg19a  39192  cdlemg27a  39201  cdlemg33b0  39210  cdlemg35  39222  cdlemg42  39238  cdlemg46  39244  trljco  39249  tendopltp  39289  cdlemi  39329  cdlemk3  39342  cdlemk10  39352  cdlemk15  39364  cdlemk1u  39368  cdlemk39  39425  cdlemk50  39461  erng1lem  39496  erngdvlem4  39500  erngdvlem4-rN  39508  dialss  39555  dia2dimlem1  39573  dia2dimlem10  39582  dia2dimlem12  39584  cdlemm10N  39627  djajN  39646  diblss  39679  cdlemn2  39704  dihjustlem  39725  dihord1  39727  dihord2pre2  39735  dib2dim  39752  dih2dimb  39753  dih2dimbALTN  39754  dihopelvalcpre  39757  dihord5b  39768  dihord5apre  39771  dihmeetlem1N  39799  dihglblem5apreN  39800  dihglblem2N  39803  dihmeetlem2N  39808  dihmeetlem3N  39814  lclkrlem2f  40021  lclkrlem2v  40037  lclkrslem2  40047  lcfrlem25  40076  lcfrlem35  40086  mapdlsm  40173  evlsval3  40787  numdenexp  40866  disjinfi  43500  fourierdlem54  44487  fourierdlem76  44509
  Copyright terms: Public domain W3C validator