Theorem mpbi2and 712

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  9355  hartogslem1  9423  cantnfp1lem3  9565  oemapwe  9579  cantnffval2  9580  mulne0d  11761  flflp1  13703  flval2  13710  remim  15016  ntrivcvgtail  15799  divalgmod  16309  divnumden  16651  numdensq  16657  numdenexp  16663  prmdivdiv  16690  4sqlem7  16848  isposd  18220  poslubmo  18307  posglbmo  18308  latasymd  18343  latjidm  18360  latmidm  18372  latledi  18375  latjass  18381  mod1ile  18391  isglbd  18407  lubun  18413  ismgmid2  18568  oppginv  19264  slwhash  19529  lsmmod  19580  iscmnd  19699  dprd2da  19949  dmdprdsplit2lem  19952  dprdsplit  19955  pgpfac1lem1  19981  ringurd  20096  imasring  20241  subrg1  20490  isdrngd  20673  isdrngdOLD  20675  lsmsp  21013  lspprabs  21022  lsmcv  21071  psr1  21901  mat1  22355  lmcn2  23557  dvdsq1p  26088  wilthlem2  26999  dchr1  27188  ismir  28630  vdgfrgrgt2  30268  atcvatlem  32355  ressprs  32937  rprmasso  33480  rprmasso3  33482  zarclssn  33876  ordtconnlem1  33927  cvmliftphtlem  35329  cvmlift3lem6  35336  cvmlift3lem9  35339  poimirlem13  37652  poimirlem14  37653  lsatexch  39061  lsatcvatlem  39067  oldmm1  39235  olj01  39243  olm01  39254  cvrcmp  39301  atcvreq0  39332  cvlexchb1  39348  cvlcvr1  39357  exatleN  39422  hlrelat3  39430  cvrval3  39431  cvratlem  39439  atlelt  39456  cvrat3  39460  2atjm  39463  atbtwn  39464  hlatexch3N  39498  hlatexch4  39499  2llnmat  39542  2atm  39545  lplnexllnN  39582  2llnjaN  39584  4atlem11b  39626  4atlem12b  39629  2lplnja  39637  dalem1  39677  dalemcea  39678  dalem3  39682  dalem8  39688  dalem16  39697  dalem17  39698  dalem21  39712  dalem25  39716  dalem39  39729  dalem54  39744  dalem55  39745  dalem57  39747  dalem60  39750  2lnat  39802  2atm2atN  39803  2llnma1b  39804  cdlema1N  39809  paddasslem12  39849  paddasslem13  39850  pmodlem1  39864  dalawlem2  39890  dalawlem3  39891  dalawlem5  39893  dalawlem6  39894  dalawlem8  39896  dalawlem11  39899  dalawlem12  39900  osumcllem1N  39974  lhp2lt  40019  lhpexle2lem  40027  lhpexle3lem  40029  lhpocnle  40034  lhpat3  40064  4atexlemtlw  40085  4atexlemnclw  40088  4atexlemcnd  40090  lautj  40111  lautm  40112  trlval3  40205  cdlemc5  40213  cdlemd3  40218  cdleme3g  40252  cdleme3h  40253  cdleme7d  40264  cdleme11c  40279  cdleme11k  40286  cdleme15d  40295  cdleme16e  40300  cdleme16f  40301  cdleme17b  40305  cdlemednpq  40317  cdleme19a  40321  cdleme20j  40336  cdleme21c  40345  cdleme22aa  40357  cdleme22b  40359  cdleme22cN  40360  cdleme22d  40361  cdleme23c  40369  cdleme28a  40388  cdleme35a  40466  cdleme35b  40468  cdleme35f  40472  cdleme42i  40501  cdlemeg46req  40547  cdlemf2  40580  cdlemg4c  40630  cdlemg6c  40638  cdlemg8b  40646  cdlemg10  40659  cdlemg11b  40660  cdlemg12f  40666  cdlemg13a  40669  cdlemg17a  40679  cdlemg17dALTN  40682  cdlemg18b  40697  cdlemg19a  40701  cdlemg27a  40710  cdlemg33b0  40719  cdlemg35  40731  cdlemg42  40747  cdlemg46  40753  trljco  40758  tendopltp  40798  cdlemi  40838  cdlemk3  40851  cdlemk10  40861  cdlemk15  40873  cdlemk1u  40877  cdlemk39  40934  cdlemk50  40970  erng1lem  41005  erngdvlem4  41009  erngdvlem4-rN  41017  dialss  41064  dia2dimlem1  41082  dia2dimlem10  41091  dia2dimlem12  41093  cdlemm10N  41136  djajN  41155  diblss  41188  cdlemn2  41213  dihjustlem  41234  dihord1  41236  dihord2pre2  41244  dib2dim  41261  dih2dimb  41262  dih2dimbALTN  41263  dihopelvalcpre  41266  dihord5b  41277  dihord5apre  41280  dihmeetlem1N  41308  dihglblem5apreN  41309  dihglblem2N  41312  dihmeetlem2N  41317  dihmeetlem3N  41323  lclkrlem2f  41530  lclkrlem2v  41546  lclkrslem2  41556  lcfrlem25  41585  lcfrlem35  41595  mapdlsm  41682  evlsval3  42571  disjinfi  45208  fourierdlem54  46177  fourierdlem76  46199  uhgrimisgrgriclem  47940