Theorem mpbi2and 713

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 232	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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 207  df-an 396

This theorem is referenced by:  supiso  9391  hartogslem1  9459  cantnfp1lem3  9601  oemapwe  9615  cantnffval2  9616  mulne0d  11801  flflp1  13739  flval2  13746  remim  15052  ntrivcvgtail  15835  divalgmod  16345  divnumden  16687  numdensq  16693  numdenexp  16699  prmdivdiv  16726  4sqlem7  16884  isposd  18257  poslubmo  18344  posglbmo  18345  latasymd  18380  latjidm  18397  latmidm  18409  latledi  18412  latjass  18418  mod1ile  18428  isglbd  18444  lubun  18450  ismgmid2  18605  oppginv  19300  slwhash  19565  lsmmod  19616  iscmnd  19735  dprd2da  19985  dmdprdsplit2lem  19988  dprdsplit  19991  pgpfac1lem1  20017  ringurd  20132  imasring  20278  subrg1  20527  isdrngd  20710  isdrngdOLD  20712  lsmsp  21050  lspprabs  21059  lsmcv  21108  psr1  21938  evlsval3  22056  mat1  22403  lmcn2  23605  dvdsq1p  26136  wilthlem2  27047  dchr1  27236  ismir  28743  vdgfrgrgt2  30385  atcvatlem  32472  ressprs  33058  rprmasso  33617  rprmasso3  33619  zarclssn  34050  ordtconnlem1  34101  cvmliftphtlem  35530  cvmlift3lem6  35537  cvmlift3lem9  35540  poimirlem13  37873  poimirlem14  37874  lsatexch  39408  lsatcvatlem  39414  oldmm1  39582  olj01  39590  olm01  39601  cvrcmp  39648  atcvreq0  39679  cvlexchb1  39695  cvlcvr1  39704  exatleN  39769  hlrelat3  39777  cvrval3  39778  cvratlem  39786  atlelt  39803  cvrat3  39807  2atjm  39810  atbtwn  39811  hlatexch3N  39845  hlatexch4  39846  2llnmat  39889  2atm  39892  lplnexllnN  39929  2llnjaN  39931  4atlem11b  39973  4atlem12b  39976  2lplnja  39984  dalem1  40024  dalemcea  40025  dalem3  40029  dalem8  40035  dalem16  40044  dalem17  40045  dalem21  40059  dalem25  40063  dalem39  40076  dalem54  40091  dalem55  40092  dalem57  40094  dalem60  40097  2lnat  40149  2atm2atN  40150  2llnma1b  40151  cdlema1N  40156  paddasslem12  40196  paddasslem13  40197  pmodlem1  40211  dalawlem2  40237  dalawlem3  40238  dalawlem5  40240  dalawlem6  40241  dalawlem8  40243  dalawlem11  40246  dalawlem12  40247  osumcllem1N  40321  lhp2lt  40366  lhpexle2lem  40374  lhpexle3lem  40376  lhpocnle  40381  lhpat3  40411  4atexlemtlw  40432  4atexlemnclw  40435  4atexlemcnd  40437  lautj  40458  lautm  40459  trlval3  40552  cdlemc5  40560  cdlemd3  40565  cdleme3g  40599  cdleme3h  40600  cdleme7d  40611  cdleme11c  40626  cdleme11k  40633  cdleme15d  40642  cdleme16e  40647  cdleme16f  40648  cdleme17b  40652  cdlemednpq  40664  cdleme19a  40668  cdleme20j  40683  cdleme21c  40692  cdleme22aa  40704  cdleme22b  40706  cdleme22cN  40707  cdleme22d  40708  cdleme23c  40716  cdleme28a  40735  cdleme35a  40813  cdleme35b  40815  cdleme35f  40819  cdleme42i  40848  cdlemeg46req  40894  cdlemf2  40927  cdlemg4c  40977  cdlemg6c  40985  cdlemg8b  40993  cdlemg10  41006  cdlemg11b  41007  cdlemg12f  41013  cdlemg13a  41016  cdlemg17a  41026  cdlemg17dALTN  41029  cdlemg18b  41044  cdlemg19a  41048  cdlemg27a  41057  cdlemg33b0  41066  cdlemg35  41078  cdlemg42  41094  cdlemg46  41100  trljco  41105  tendopltp  41145  cdlemi  41185  cdlemk3  41198  cdlemk10  41208  cdlemk15  41220  cdlemk1u  41224  cdlemk39  41281  cdlemk50  41317  erng1lem  41352  erngdvlem4  41356  erngdvlem4-rN  41364  dialss  41411  dia2dimlem1  41429  dia2dimlem10  41438  dia2dimlem12  41440  cdlemm10N  41483  djajN  41502  diblss  41535  cdlemn2  41560  dihjustlem  41581  dihord1  41583  dihord2pre2  41591  dib2dim  41608  dih2dimb  41609  dih2dimbALTN  41610  dihopelvalcpre  41613  dihord5b  41624  dihord5apre  41627  dihmeetlem1N  41655  dihglblem5apreN  41656  dihglblem2N  41659  dihmeetlem2N  41664  dihmeetlem3N  41670  lclkrlem2f  41877  lclkrlem2v  41893  lclkrslem2  41903  lcfrlem25  41932  lcfrlem35  41942  mapdlsm  42029  disjinfi  45540  fourierdlem54  46507  fourierdlem76  46529  uhgrimisgrgriclem  48279