Theorem mpbi2and 709

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

Step	Hyp	Ref	Expression
1		mpbi2and.1	. . 3 ⊢ (𝜑 → 𝜓)
2		mpbi2and.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 511	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		mpbi2and.3	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ 𝜃))
5	3, 4	mpbid 231	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395

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 396

This theorem is referenced by:  supiso  9476  hartogslem1  9543  cantnfp1lem3  9681  oemapwe  9695  cantnffval2  9696  mulne0d  11873  flflp1  13779  flval2  13786  remim  15071  ntrivcvgtail  15853  divalgmod  16356  divnumden  16691  numdensq  16697  prmdivdiv  16727  4sqlem7  16884  isposd  18283  poslubmo  18371  posglbmo  18372  latasymd  18405  latjidm  18422  latmidm  18434  latledi  18437  latjass  18443  mod1ile  18453  isglbd  18469  lubun  18475  ismgmid2  18596  oppginv  19271  slwhash  19537  lsmmod  19588  iscmnd  19707  dprd2da  19957  dmdprdsplit2lem  19960  dprdsplit  19963  pgpfac1lem1  19989  ringurd  20083  imasring  20222  subrg1  20476  isdrngd  20537  isdrngdOLD  20539  lsmsp  20845  lspprabs  20854  lsmcv  20903  psr1  21756  mat1  22182  lmcn2  23386  dvdsq1p  25927  wilthlem2  26824  dchr1  27011  ismir  28192  vdgfrgrgt2  29833  atcvatlem  31920  ressprs  32415  zarclssn  33166  ordtconnlem1  33217  cvmliftphtlem  34621  cvmlift3lem6  34628  cvmlift3lem9  34631  poimirlem13  36817  poimirlem14  36818  lsatexch  38229  lsatcvatlem  38235  oldmm1  38403  olj01  38411  olm01  38422  cvrcmp  38469  atcvreq0  38500  cvlexchb1  38516  cvlcvr1  38525  exatleN  38591  hlrelat3  38599  cvrval3  38600  cvratlem  38608  atlelt  38625  cvrat3  38629  2atjm  38632  atbtwn  38633  hlatexch3N  38667  hlatexch4  38668  2llnmat  38711  2atm  38714  lplnexllnN  38751  2llnjaN  38753  4atlem11b  38795  4atlem12b  38798  2lplnja  38806  dalem1  38846  dalemcea  38847  dalem3  38851  dalem8  38857  dalem16  38866  dalem17  38867  dalem21  38881  dalem25  38885  dalem39  38898  dalem54  38913  dalem55  38914  dalem57  38916  dalem60  38919  2lnat  38971  2atm2atN  38972  2llnma1b  38973  cdlema1N  38978  paddasslem12  39018  paddasslem13  39019  pmodlem1  39033  dalawlem2  39059  dalawlem3  39060  dalawlem5  39062  dalawlem6  39063  dalawlem8  39065  dalawlem11  39068  dalawlem12  39069  osumcllem1N  39143  lhp2lt  39188  lhpexle2lem  39196  lhpexle3lem  39198  lhpocnle  39203  lhpat3  39233  4atexlemtlw  39254  4atexlemnclw  39257  4atexlemcnd  39259  lautj  39280  lautm  39281  trlval3  39374  cdlemc5  39382  cdlemd3  39387  cdleme3g  39421  cdleme3h  39422  cdleme7d  39433  cdleme11c  39448  cdleme11k  39455  cdleme15d  39464  cdleme16e  39469  cdleme16f  39470  cdleme17b  39474  cdlemednpq  39486  cdleme19a  39490  cdleme20j  39505  cdleme21c  39514  cdleme22aa  39526  cdleme22b  39528  cdleme22cN  39529  cdleme22d  39530  cdleme23c  39538  cdleme28a  39557  cdleme35a  39635  cdleme35b  39637  cdleme35f  39641  cdleme42i  39670  cdlemeg46req  39716  cdlemf2  39749  cdlemg4c  39799  cdlemg6c  39807  cdlemg8b  39815  cdlemg10  39828  cdlemg11b  39829  cdlemg12f  39835  cdlemg13a  39838  cdlemg17a  39848  cdlemg17dALTN  39851  cdlemg18b  39866  cdlemg19a  39870  cdlemg27a  39879  cdlemg33b0  39888  cdlemg35  39900  cdlemg42  39916  cdlemg46  39922  trljco  39927  tendopltp  39967  cdlemi  40007  cdlemk3  40020  cdlemk10  40030  cdlemk15  40042  cdlemk1u  40046  cdlemk39  40103  cdlemk50  40139  erng1lem  40174  erngdvlem4  40178  erngdvlem4-rN  40186  dialss  40233  dia2dimlem1  40251  dia2dimlem10  40260  dia2dimlem12  40262  cdlemm10N  40305  djajN  40324  diblss  40357  cdlemn2  40382  dihjustlem  40403  dihord1  40405  dihord2pre2  40413  dib2dim  40430  dih2dimb  40431  dih2dimbALTN  40432  dihopelvalcpre  40435  dihord5b  40446  dihord5apre  40449  dihmeetlem1N  40477  dihglblem5apreN  40478  dihglblem2N  40481  dihmeetlem2N  40486  dihmeetlem3N  40492  lclkrlem2f  40699  lclkrlem2v  40715  lclkrslem2  40725  lcfrlem25  40754  lcfrlem35  40764  mapdlsm  40851  evlsval3  41446  numdenexp  41543  disjinfi  44202  fourierdlem54  45187  fourierdlem76  45209