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  9389  hartogslem1  9457  cantnfp1lem3  9601  oemapwe  9615  cantnffval2  9616  mulne0d  11802  flflp1  13766  flval2  13773  remim  15079  ntrivcvgtail  15865  divalgmod  16375  divnumden  16718  numdensq  16724  numdenexp  16730  prmdivdiv  16757  4sqlem7  16915  isposd  18288  poslubmo  18375  posglbmo  18376  latasymd  18411  latjidm  18428  latmidm  18440  latledi  18443  latjass  18449  mod1ile  18459  isglbd  18475  lubun  18481  ismgmid2  18636  oppginv  19334  slwhash  19599  lsmmod  19650  iscmnd  19769  dprd2da  20019  dmdprdsplit2lem  20022  dprdsplit  20025  pgpfac1lem1  20051  ringurd  20166  imasring  20310  subrg1  20559  isdrngd  20742  isdrngdOLD  20744  lsmsp  21081  lspprabs  21090  lsmcv  21139  psr1  21949  evlsval3  22067  mat1  22412  lmcn2  23614  dvdsq1p  26128  wilthlem2  27032  dchr1  27220  ismir  28727  vdgfrgrgt2  30368  atcvatlem  32456  ressprs  33026  rprmasso  33585  rprmasso3  33587  zarclssn  34017  ordtconnlem1  34068  cvmliftphtlem  35499  cvmlift3lem6  35506  cvmlift3lem9  35509  poimirlem13  37954  poimirlem14  37955  lsatexch  39489  lsatcvatlem  39495  oldmm1  39663  olj01  39671  olm01  39682  cvrcmp  39729  atcvreq0  39760  cvlexchb1  39776  cvlcvr1  39785  exatleN  39850  hlrelat3  39858  cvrval3  39859  cvratlem  39867  atlelt  39884  cvrat3  39888  2atjm  39891  atbtwn  39892  hlatexch3N  39926  hlatexch4  39927  2llnmat  39970  2atm  39973  lplnexllnN  40010  2llnjaN  40012  4atlem11b  40054  4atlem12b  40057  2lplnja  40065  dalem1  40105  dalemcea  40106  dalem3  40110  dalem8  40116  dalem16  40125  dalem17  40126  dalem21  40140  dalem25  40144  dalem39  40157  dalem54  40172  dalem55  40173  dalem57  40175  dalem60  40178  2lnat  40230  2atm2atN  40231  2llnma1b  40232  cdlema1N  40237  paddasslem12  40277  paddasslem13  40278  pmodlem1  40292  dalawlem2  40318  dalawlem3  40319  dalawlem5  40321  dalawlem6  40322  dalawlem8  40324  dalawlem11  40327  dalawlem12  40328  osumcllem1N  40402  lhp2lt  40447  lhpexle2lem  40455  lhpexle3lem  40457  lhpocnle  40462  lhpat3  40492  4atexlemtlw  40513  4atexlemnclw  40516  4atexlemcnd  40518  lautj  40539  lautm  40540  trlval3  40633  cdlemc5  40641  cdlemd3  40646  cdleme3g  40680  cdleme3h  40681  cdleme7d  40692  cdleme11c  40707  cdleme11k  40714  cdleme15d  40723  cdleme16e  40728  cdleme16f  40729  cdleme17b  40733  cdlemednpq  40745  cdleme19a  40749  cdleme20j  40764  cdleme21c  40773  cdleme22aa  40785  cdleme22b  40787  cdleme22cN  40788  cdleme22d  40789  cdleme23c  40797  cdleme28a  40816  cdleme35a  40894  cdleme35b  40896  cdleme35f  40900  cdleme42i  40929  cdlemeg46req  40975  cdlemf2  41008  cdlemg4c  41058  cdlemg6c  41066  cdlemg8b  41074  cdlemg10  41087  cdlemg11b  41088  cdlemg12f  41094  cdlemg13a  41097  cdlemg17a  41107  cdlemg17dALTN  41110  cdlemg18b  41125  cdlemg19a  41129  cdlemg27a  41138  cdlemg33b0  41147  cdlemg35  41159  cdlemg42  41175  cdlemg46  41181  trljco  41186  tendopltp  41226  cdlemi  41266  cdlemk3  41279  cdlemk10  41289  cdlemk15  41301  cdlemk1u  41305  cdlemk39  41362  cdlemk50  41398  erng1lem  41433  erngdvlem4  41437  erngdvlem4-rN  41445  dialss  41492  dia2dimlem1  41510  dia2dimlem10  41519  dia2dimlem12  41521  cdlemm10N  41564  djajN  41583  diblss  41616  cdlemn2  41641  dihjustlem  41662  dihord1  41664  dihord2pre2  41672  dib2dim  41689  dih2dimb  41690  dih2dimbALTN  41691  dihopelvalcpre  41694  dihord5b  41705  dihord5apre  41708  dihmeetlem1N  41736  dihglblem5apreN  41737  dihglblem2N  41740  dihmeetlem2N  41745  dihmeetlem3N  41751  lclkrlem2f  41958  lclkrlem2v  41974  lclkrslem2  41984  lcfrlem25  42013  lcfrlem35  42023  mapdlsm  42110  disjinfi  45622  fourierdlem54  46588  fourierdlem76  46610  uhgrimisgrgriclem  48406