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  9493  hartogslem1  9561  cantnfp1lem3  9699  oemapwe  9713  cantnffval2  9714  mulne0d  11894  flflp1  13829  flval2  13836  remim  15141  ntrivcvgtail  15921  divalgmod  16430  divnumden  16772  numdensq  16778  numdenexp  16784  prmdivdiv  16811  4sqlem7  16969  isposd  18339  poslubmo  18426  posglbmo  18427  latasymd  18460  latjidm  18477  latmidm  18489  latledi  18492  latjass  18498  mod1ile  18508  isglbd  18524  lubun  18530  ismgmid2  18651  oppginv  19347  slwhash  19610  lsmmod  19661  iscmnd  19780  dprd2da  20030  dmdprdsplit2lem  20033  dprdsplit  20036  pgpfac1lem1  20062  ringurd  20150  imasring  20295  subrg1  20547  isdrngd  20730  isdrngdOLD  20732  lsmsp  21049  lspprabs  21058  lsmcv  21107  psr1  21936  mat1  22390  lmcn2  23592  dvdsq1p  26125  wilthlem2  27036  dchr1  27225  ismir  28643  vdgfrgrgt2  30284  atcvatlem  32371  ressprs  32949  rprmasso  33545  rprmasso3  33547  zarclssn  33909  ordtconnlem1  33960  cvmliftphtlem  35344  cvmlift3lem6  35351  cvmlift3lem9  35354  poimirlem13  37662  poimirlem14  37663  lsatexch  39066  lsatcvatlem  39072  oldmm1  39240  olj01  39248  olm01  39259  cvrcmp  39306  atcvreq0  39337  cvlexchb1  39353  cvlcvr1  39362  exatleN  39428  hlrelat3  39436  cvrval3  39437  cvratlem  39445  atlelt  39462  cvrat3  39466  2atjm  39469  atbtwn  39470  hlatexch3N  39504  hlatexch4  39505  2llnmat  39548  2atm  39551  lplnexllnN  39588  2llnjaN  39590  4atlem11b  39632  4atlem12b  39635  2lplnja  39643  dalem1  39683  dalemcea  39684  dalem3  39688  dalem8  39694  dalem16  39703  dalem17  39704  dalem21  39718  dalem25  39722  dalem39  39735  dalem54  39750  dalem55  39751  dalem57  39753  dalem60  39756  2lnat  39808  2atm2atN  39809  2llnma1b  39810  cdlema1N  39815  paddasslem12  39855  paddasslem13  39856  pmodlem1  39870  dalawlem2  39896  dalawlem3  39897  dalawlem5  39899  dalawlem6  39900  dalawlem8  39902  dalawlem11  39905  dalawlem12  39906  osumcllem1N  39980  lhp2lt  40025  lhpexle2lem  40033  lhpexle3lem  40035  lhpocnle  40040  lhpat3  40070  4atexlemtlw  40091  4atexlemnclw  40094  4atexlemcnd  40096  lautj  40117  lautm  40118  trlval3  40211  cdlemc5  40219  cdlemd3  40224  cdleme3g  40258  cdleme3h  40259  cdleme7d  40270  cdleme11c  40285  cdleme11k  40292  cdleme15d  40301  cdleme16e  40306  cdleme16f  40307  cdleme17b  40311  cdlemednpq  40323  cdleme19a  40327  cdleme20j  40342  cdleme21c  40351  cdleme22aa  40363  cdleme22b  40365  cdleme22cN  40366  cdleme22d  40367  cdleme23c  40375  cdleme28a  40394  cdleme35a  40472  cdleme35b  40474  cdleme35f  40478  cdleme42i  40507  cdlemeg46req  40553  cdlemf2  40586  cdlemg4c  40636  cdlemg6c  40644  cdlemg8b  40652  cdlemg10  40665  cdlemg11b  40666  cdlemg12f  40672  cdlemg13a  40675  cdlemg17a  40685  cdlemg17dALTN  40688  cdlemg18b  40703  cdlemg19a  40707  cdlemg27a  40716  cdlemg33b0  40725  cdlemg35  40737  cdlemg42  40753  cdlemg46  40759  trljco  40764  tendopltp  40804  cdlemi  40844  cdlemk3  40857  cdlemk10  40867  cdlemk15  40879  cdlemk1u  40883  cdlemk39  40940  cdlemk50  40976  erng1lem  41011  erngdvlem4  41015  erngdvlem4-rN  41023  dialss  41070  dia2dimlem1  41088  dia2dimlem10  41097  dia2dimlem12  41099  cdlemm10N  41142  djajN  41161  diblss  41194  cdlemn2  41219  dihjustlem  41240  dihord1  41242  dihord2pre2  41250  dib2dim  41267  dih2dimb  41268  dih2dimbALTN  41269  dihopelvalcpre  41272  dihord5b  41283  dihord5apre  41286  dihmeetlem1N  41314  dihglblem5apreN  41315  dihglblem2N  41318  dihmeetlem2N  41323  dihmeetlem3N  41329  lclkrlem2f  41536  lclkrlem2v  41552  lclkrslem2  41562  lcfrlem25  41591  lcfrlem35  41601  mapdlsm  41688  evlsval3  42557  disjinfi  45196  fourierdlem54  46169  fourierdlem76  46191  uhgrimisgrgriclem  47923