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  9380  hartogslem1  9448  cantnfp1lem3  9590  oemapwe  9604  cantnffval2  9605  mulne0d  11791  flflp1  13755  flval2  13762  remim  15068  ntrivcvgtail  15854  divalgmod  16364  divnumden  16707  numdensq  16713  numdenexp  16719  prmdivdiv  16746  4sqlem7  16904  isposd  18277  poslubmo  18364  posglbmo  18365  latasymd  18400  latjidm  18417  latmidm  18429  latledi  18432  latjass  18438  mod1ile  18448  isglbd  18464  lubun  18470  ismgmid2  18625  oppginv  19323  slwhash  19588  lsmmod  19639  iscmnd  19758  dprd2da  20008  dmdprdsplit2lem  20011  dprdsplit  20014  pgpfac1lem1  20040  ringurd  20155  imasring  20299  subrg1  20548  isdrngd  20731  isdrngdOLD  20733  lsmsp  21071  lspprabs  21080  lsmcv  21129  psr1  21958  evlsval3  22076  mat1  22421  lmcn2  23623  dvdsq1p  26140  wilthlem2  27050  dchr1  27239  ismir  28746  vdgfrgrgt2  30388  atcvatlem  32476  ressprs  33046  rprmasso  33605  rprmasso3  33607  zarclssn  34038  ordtconnlem1  34089  cvmliftphtlem  35520  cvmlift3lem6  35527  cvmlift3lem9  35530  poimirlem13  37965  poimirlem14  37966  lsatexch  39500  lsatcvatlem  39506  oldmm1  39674  olj01  39682  olm01  39693  cvrcmp  39740  atcvreq0  39771  cvlexchb1  39787  cvlcvr1  39796  exatleN  39861  hlrelat3  39869  cvrval3  39870  cvratlem  39878  atlelt  39895  cvrat3  39899  2atjm  39902  atbtwn  39903  hlatexch3N  39937  hlatexch4  39938  2llnmat  39981  2atm  39984  lplnexllnN  40021  2llnjaN  40023  4atlem11b  40065  4atlem12b  40068  2lplnja  40076  dalem1  40116  dalemcea  40117  dalem3  40121  dalem8  40127  dalem16  40136  dalem17  40137  dalem21  40151  dalem25  40155  dalem39  40168  dalem54  40183  dalem55  40184  dalem57  40186  dalem60  40189  2lnat  40241  2atm2atN  40242  2llnma1b  40243  cdlema1N  40248  paddasslem12  40288  paddasslem13  40289  pmodlem1  40303  dalawlem2  40329  dalawlem3  40330  dalawlem5  40332  dalawlem6  40333  dalawlem8  40335  dalawlem11  40338  dalawlem12  40339  osumcllem1N  40413  lhp2lt  40458  lhpexle2lem  40466  lhpexle3lem  40468  lhpocnle  40473  lhpat3  40503  4atexlemtlw  40524  4atexlemnclw  40527  4atexlemcnd  40529  lautj  40550  lautm  40551  trlval3  40644  cdlemc5  40652  cdlemd3  40657  cdleme3g  40691  cdleme3h  40692  cdleme7d  40703  cdleme11c  40718  cdleme11k  40725  cdleme15d  40734  cdleme16e  40739  cdleme16f  40740  cdleme17b  40744  cdlemednpq  40756  cdleme19a  40760  cdleme20j  40775  cdleme21c  40784  cdleme22aa  40796  cdleme22b  40798  cdleme22cN  40799  cdleme22d  40800  cdleme23c  40808  cdleme28a  40827  cdleme35a  40905  cdleme35b  40907  cdleme35f  40911  cdleme42i  40940  cdlemeg46req  40986  cdlemf2  41019  cdlemg4c  41069  cdlemg6c  41077  cdlemg8b  41085  cdlemg10  41098  cdlemg11b  41099  cdlemg12f  41105  cdlemg13a  41108  cdlemg17a  41118  cdlemg17dALTN  41121  cdlemg18b  41136  cdlemg19a  41140  cdlemg27a  41149  cdlemg33b0  41158  cdlemg35  41170  cdlemg42  41186  cdlemg46  41192  trljco  41197  tendopltp  41237  cdlemi  41277  cdlemk3  41290  cdlemk10  41300  cdlemk15  41312  cdlemk1u  41316  cdlemk39  41373  cdlemk50  41409  erng1lem  41444  erngdvlem4  41448  erngdvlem4-rN  41456  dialss  41503  dia2dimlem1  41521  dia2dimlem10  41530  dia2dimlem12  41532  cdlemm10N  41575  djajN  41594  diblss  41627  cdlemn2  41652  dihjustlem  41673  dihord1  41675  dihord2pre2  41683  dib2dim  41700  dih2dimb  41701  dih2dimbALTN  41702  dihopelvalcpre  41705  dihord5b  41716  dihord5apre  41719  dihmeetlem1N  41747  dihglblem5apreN  41748  dihglblem2N  41751  dihmeetlem2N  41756  dihmeetlem3N  41762  lclkrlem2f  41969  lclkrlem2v  41985  lclkrslem2  41995  lcfrlem25  42024  lcfrlem35  42034  mapdlsm  42121  disjinfi  45637  fourierdlem54  46603  fourierdlem76  46625  uhgrimisgrgriclem  48403