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  9434  hartogslem1  9502  cantnfp1lem3  9640  oemapwe  9654  cantnffval2  9655  mulne0d  11837  flflp1  13776  flval2  13783  remim  15090  ntrivcvgtail  15873  divalgmod  16383  divnumden  16725  numdensq  16731  numdenexp  16737  prmdivdiv  16764  4sqlem7  16922  isposd  18290  poslubmo  18377  posglbmo  18378  latasymd  18411  latjidm  18428  latmidm  18440  latledi  18443  latjass  18449  mod1ile  18459  isglbd  18475  lubun  18481  ismgmid2  18602  oppginv  19298  slwhash  19561  lsmmod  19612  iscmnd  19731  dprd2da  19981  dmdprdsplit2lem  19984  dprdsplit  19987  pgpfac1lem1  20013  ringurd  20101  imasring  20246  subrg1  20498  isdrngd  20681  isdrngdOLD  20683  lsmsp  21000  lspprabs  21009  lsmcv  21058  psr1  21887  mat1  22341  lmcn2  23543  dvdsq1p  26075  wilthlem2  26986  dchr1  27175  ismir  28593  vdgfrgrgt2  30234  atcvatlem  32321  ressprs  32897  rprmasso  33503  rprmasso3  33505  zarclssn  33870  ordtconnlem1  33921  cvmliftphtlem  35311  cvmlift3lem6  35318  cvmlift3lem9  35321  poimirlem13  37634  poimirlem14  37635  lsatexch  39043  lsatcvatlem  39049  oldmm1  39217  olj01  39225  olm01  39236  cvrcmp  39283  atcvreq0  39314  cvlexchb1  39330  cvlcvr1  39339  exatleN  39405  hlrelat3  39413  cvrval3  39414  cvratlem  39422  atlelt  39439  cvrat3  39443  2atjm  39446  atbtwn  39447  hlatexch3N  39481  hlatexch4  39482  2llnmat  39525  2atm  39528  lplnexllnN  39565  2llnjaN  39567  4atlem11b  39609  4atlem12b  39612  2lplnja  39620  dalem1  39660  dalemcea  39661  dalem3  39665  dalem8  39671  dalem16  39680  dalem17  39681  dalem21  39695  dalem25  39699  dalem39  39712  dalem54  39727  dalem55  39728  dalem57  39730  dalem60  39733  2lnat  39785  2atm2atN  39786  2llnma1b  39787  cdlema1N  39792  paddasslem12  39832  paddasslem13  39833  pmodlem1  39847  dalawlem2  39873  dalawlem3  39874  dalawlem5  39876  dalawlem6  39877  dalawlem8  39879  dalawlem11  39882  dalawlem12  39883  osumcllem1N  39957  lhp2lt  40002  lhpexle2lem  40010  lhpexle3lem  40012  lhpocnle  40017  lhpat3  40047  4atexlemtlw  40068  4atexlemnclw  40071  4atexlemcnd  40073  lautj  40094  lautm  40095  trlval3  40188  cdlemc5  40196  cdlemd3  40201  cdleme3g  40235  cdleme3h  40236  cdleme7d  40247  cdleme11c  40262  cdleme11k  40269  cdleme15d  40278  cdleme16e  40283  cdleme16f  40284  cdleme17b  40288  cdlemednpq  40300  cdleme19a  40304  cdleme20j  40319  cdleme21c  40328  cdleme22aa  40340  cdleme22b  40342  cdleme22cN  40343  cdleme22d  40344  cdleme23c  40352  cdleme28a  40371  cdleme35a  40449  cdleme35b  40451  cdleme35f  40455  cdleme42i  40484  cdlemeg46req  40530  cdlemf2  40563  cdlemg4c  40613  cdlemg6c  40621  cdlemg8b  40629  cdlemg10  40642  cdlemg11b  40643  cdlemg12f  40649  cdlemg13a  40652  cdlemg17a  40662  cdlemg17dALTN  40665  cdlemg18b  40680  cdlemg19a  40684  cdlemg27a  40693  cdlemg33b0  40702  cdlemg35  40714  cdlemg42  40730  cdlemg46  40736  trljco  40741  tendopltp  40781  cdlemi  40821  cdlemk3  40834  cdlemk10  40844  cdlemk15  40856  cdlemk1u  40860  cdlemk39  40917  cdlemk50  40953  erng1lem  40988  erngdvlem4  40992  erngdvlem4-rN  41000  dialss  41047  dia2dimlem1  41065  dia2dimlem10  41074  dia2dimlem12  41076  cdlemm10N  41119  djajN  41138  diblss  41171  cdlemn2  41196  dihjustlem  41217  dihord1  41219  dihord2pre2  41227  dib2dim  41244  dih2dimb  41245  dih2dimbALTN  41246  dihopelvalcpre  41249  dihord5b  41260  dihord5apre  41263  dihmeetlem1N  41291  dihglblem5apreN  41292  dihglblem2N  41295  dihmeetlem2N  41300  dihmeetlem3N  41306  lclkrlem2f  41513  lclkrlem2v  41529  lclkrslem2  41539  lcfrlem25  41568  lcfrlem35  41578  mapdlsm  41665  evlsval3  42554  disjinfi  45193  fourierdlem54  46165  fourierdlem76  46187  uhgrimisgrgriclem  47934