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  9513  hartogslem1  9580  cantnfp1lem3  9718  oemapwe  9732  cantnffval2  9733  mulne0d  11913  flflp1  13844  flval2  13851  remim  15153  ntrivcvgtail  15933  divalgmod  16440  divnumden  16782  numdensq  16788  numdenexp  16794  prmdivdiv  16821  4sqlem7  16978  isposd  18381  poslubmo  18469  posglbmo  18470  latasymd  18503  latjidm  18520  latmidm  18532  latledi  18535  latjass  18541  mod1ile  18551  isglbd  18567  lubun  18573  ismgmid2  18694  oppginv  19393  slwhash  19657  lsmmod  19708  iscmnd  19827  dprd2da  20077  dmdprdsplit2lem  20080  dprdsplit  20083  pgpfac1lem1  20109  ringurd  20203  imasring  20344  subrg1  20599  isdrngd  20782  isdrngdOLD  20784  lsmsp  21103  lspprabs  21112  lsmcv  21161  psr1  22009  mat1  22469  lmcn2  23673  dvdsq1p  26217  wilthlem2  27127  dchr1  27316  ismir  28682  vdgfrgrgt2  30327  atcvatlem  32414  ressprs  32939  rprmasso  33533  rprmasso3  33535  zarclssn  33834  ordtconnlem1  33885  cvmliftphtlem  35302  cvmlift3lem6  35309  cvmlift3lem9  35312  poimirlem13  37620  poimirlem14  37621  lsatexch  39025  lsatcvatlem  39031  oldmm1  39199  olj01  39207  olm01  39218  cvrcmp  39265  atcvreq0  39296  cvlexchb1  39312  cvlcvr1  39321  exatleN  39387  hlrelat3  39395  cvrval3  39396  cvratlem  39404  atlelt  39421  cvrat3  39425  2atjm  39428  atbtwn  39429  hlatexch3N  39463  hlatexch4  39464  2llnmat  39507  2atm  39510  lplnexllnN  39547  2llnjaN  39549  4atlem11b  39591  4atlem12b  39594  2lplnja  39602  dalem1  39642  dalemcea  39643  dalem3  39647  dalem8  39653  dalem16  39662  dalem17  39663  dalem21  39677  dalem25  39681  dalem39  39694  dalem54  39709  dalem55  39710  dalem57  39712  dalem60  39715  2lnat  39767  2atm2atN  39768  2llnma1b  39769  cdlema1N  39774  paddasslem12  39814  paddasslem13  39815  pmodlem1  39829  dalawlem2  39855  dalawlem3  39856  dalawlem5  39858  dalawlem6  39859  dalawlem8  39861  dalawlem11  39864  dalawlem12  39865  osumcllem1N  39939  lhp2lt  39984  lhpexle2lem  39992  lhpexle3lem  39994  lhpocnle  39999  lhpat3  40029  4atexlemtlw  40050  4atexlemnclw  40053  4atexlemcnd  40055  lautj  40076  lautm  40077  trlval3  40170  cdlemc5  40178  cdlemd3  40183  cdleme3g  40217  cdleme3h  40218  cdleme7d  40229  cdleme11c  40244  cdleme11k  40251  cdleme15d  40260  cdleme16e  40265  cdleme16f  40266  cdleme17b  40270  cdlemednpq  40282  cdleme19a  40286  cdleme20j  40301  cdleme21c  40310  cdleme22aa  40322  cdleme22b  40324  cdleme22cN  40325  cdleme22d  40326  cdleme23c  40334  cdleme28a  40353  cdleme35a  40431  cdleme35b  40433  cdleme35f  40437  cdleme42i  40466  cdlemeg46req  40512  cdlemf2  40545  cdlemg4c  40595  cdlemg6c  40603  cdlemg8b  40611  cdlemg10  40624  cdlemg11b  40625  cdlemg12f  40631  cdlemg13a  40634  cdlemg17a  40644  cdlemg17dALTN  40647  cdlemg18b  40662  cdlemg19a  40666  cdlemg27a  40675  cdlemg33b0  40684  cdlemg35  40696  cdlemg42  40712  cdlemg46  40718  trljco  40723  tendopltp  40763  cdlemi  40803  cdlemk3  40816  cdlemk10  40826  cdlemk15  40838  cdlemk1u  40842  cdlemk39  40899  cdlemk50  40935  erng1lem  40970  erngdvlem4  40974  erngdvlem4-rN  40982  dialss  41029  dia2dimlem1  41047  dia2dimlem10  41056  dia2dimlem12  41058  cdlemm10N  41101  djajN  41120  diblss  41153  cdlemn2  41178  dihjustlem  41199  dihord1  41201  dihord2pre2  41209  dib2dim  41226  dih2dimb  41227  dih2dimbALTN  41228  dihopelvalcpre  41231  dihord5b  41242  dihord5apre  41245  dihmeetlem1N  41273  dihglblem5apreN  41274  dihglblem2N  41277  dihmeetlem2N  41282  dihmeetlem3N  41288  lclkrlem2f  41495  lclkrlem2v  41511  lclkrslem2  41521  lcfrlem25  41550  lcfrlem35  41560  mapdlsm  41647  evlsval3  42546  disjinfi  45135  fourierdlem54  46116  fourierdlem76  46138  uhgrimisgrgriclem  47836