Theorem mpbi2and 724

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 520	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		mpbi2and.3	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ 𝜃))
5	3, 4	mpbid 235	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  supiso  9424  hartogslem1  9492  cantnfp1lem3  9637  oemapwe  9651  cantnffval2  9652  mulne0d  11854  flflp1  13831  flval2  13838  remim  15158  ntrivcvgtail  15944  divalgmod  16454  divnumden  16797  numdensq  16803  numdenexp  16809  prmdivdiv  16836  4sqlem7  16994  isposd  18368  poslubmo  18455  posglbmo  18456  latasymd  18491  latjidm  18508  latmidm  18520  latledi  18523  latjass  18529  mod1ile  18539  isglbd  18555  lubun  18561  ismgmid2  18716  oppginv  19420  slwhash  19685  lsmmod  19736  iscmnd  19855  dprd2da  20105  dmdprdsplit2lem  20108  dprdsplit  20111  pgpfac1lem1  20137  ringurd  20258  imasring  20403  subrg1  20658  isdrngd  20838  isdrngdOLD  20840  lsmsp  21176  lspprabs  21185  lsmcv  21234  psr1  22080  evlsval3  22200  mat1  22565  lmcn2  23767  dvdsq1p  26281  wilthlem2  27191  dchr1  27379  ismir  28890  vdgfrgrgt2  30558  atcvatlem  32646  ressprs  33199  rprmasso  33732  rprmasso3  33734  zarclssn  34180  ordtconnlem1  34231  cvmliftphtlem  35680  cvmlift3lem6  35687  cvmlift3lem9  35690  poimirlem13  38144  poimirlem14  38145  lsatexch  39679  lsatcvatlem  39685  oldmm1  39853  olj01  39861  olm01  39872  cvrcmp  39919  atcvreq0  39950  cvlexchb1  39966  cvlcvr1  39975  exatleN  40040  hlrelat3  40048  cvrval3  40049  cvratlem  40057  atlelt  40074  cvrat3  40078  2atjm  40081  atbtwn  40082  hlatexch3N  40116  hlatexch4  40117  2llnmat  40160  2atm  40163  lplnexllnN  40200  2llnjaN  40202  4atlem11b  40244  4atlem12b  40247  2lplnja  40255  dalem1  40295  dalemcea  40296  dalem3  40300  dalem8  40306  dalem16  40315  dalem17  40316  dalem21  40330  dalem25  40334  dalem39  40347  dalem54  40362  dalem55  40363  dalem57  40365  dalem60  40368  2lnat  40420  2atm2atN  40421  2llnma1b  40422  cdlema1N  40427  paddasslem12  40467  paddasslem13  40468  pmodlem1  40482  dalawlem2  40508  dalawlem3  40509  dalawlem5  40511  dalawlem6  40512  dalawlem8  40514  dalawlem11  40517  dalawlem12  40518  osumcllem1N  40592  lhp2lt  40637  lhpexle2lem  40645  lhpexle3lem  40647  lhpocnle  40652  lhpat3  40682  4atexlemtlw  40703  4atexlemnclw  40706  4atexlemcnd  40708  lautj  40729  lautm  40730  trlval3  40823  cdlemc5  40831  cdlemd3  40836  cdleme3g  40870  cdleme3h  40871  cdleme7d  40882  cdleme11c  40897  cdleme11k  40904  cdleme15d  40913  cdleme16e  40918  cdleme16f  40919  cdleme17b  40923  cdlemednpq  40935  cdleme19a  40939  cdleme20j  40954  cdleme21c  40963  cdleme22aa  40975  cdleme22b  40977  cdleme22cN  40978  cdleme22d  40979  cdleme23c  40987  cdleme28a  41006  cdleme35a  41084  cdleme35b  41086  cdleme35f  41090  cdleme42i  41119  cdlemeg46req  41165  cdlemf2  41198  cdlemg4c  41248  cdlemg6c  41256  cdlemg8b  41264  cdlemg10  41277  cdlemg11b  41278  cdlemg12f  41284  cdlemg13a  41287  cdlemg17a  41297  cdlemg17dALTN  41300  cdlemg18b  41315  cdlemg19a  41319  cdlemg27a  41328  cdlemg33b0  41337  cdlemg35  41349  cdlemg42  41365  cdlemg46  41371  trljco  41376  tendopltp  41416  cdlemi  41456  cdlemk3  41469  cdlemk10  41479  cdlemk15  41491  cdlemk1u  41495  cdlemk39  41552  cdlemk50  41588  erng1lem  41623  erngdvlem4  41627  erngdvlem4-rN  41635  dialss  41682  dia2dimlem1  41700  dia2dimlem10  41709  dia2dimlem12  41711  cdlemm10N  41754  djajN  41773  diblss  41806  cdlemn2  41831  dihjustlem  41852  dihord1  41854  dihord2pre2  41862  dib2dim  41879  dih2dimb  41880  dih2dimbALTN  41881  dihopelvalcpre  41884  dihord5b  41895  dihord5apre  41898  dihmeetlem1N  41926  dihglblem5apreN  41927  dihglblem2N  41930  dihmeetlem2N  41935  dihmeetlem3N  41941  lclkrlem2f  42148  lclkrlem2v  42164  lclkrslem2  42174  lcfrlem25  42203  lcfrlem35  42213  mapdlsm  42300  disjinfi  45768  fourierdlem54  46732  fourierdlem76  46754  uhgrimisgrgriclem  48550