Theorem mpbi2and 709

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 512	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		mpbi2and.3	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ 𝜃))
5	3, 4	mpbid 231	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  supiso  9243  hartogslem1  9310  cantnfp1lem3  9447  oemapwe  9461  cantnffval2  9462  mulne0d  11636  flflp1  13536  flval2  13543  remim  14837  ntrivcvgtail  15621  divalgmod  16124  divnumden  16461  numdensq  16467  prmdivdiv  16497  4sqlem7  16654  isposd  18050  poslubmo  18138  posglbmo  18139  latasymd  18172  latjidm  18189  latmidm  18201  latledi  18204  latjass  18210  mod1ile  18220  isglbd  18236  lubun  18242  ismgmid2  18361  oppginv  18975  slwhash  19238  lsmmod  19290  iscmnd  19408  dprd2da  19654  dmdprdsplit2lem  19657  dprdsplit  19660  pgpfac1lem1  19686  imasring  19867  isdrngd  20025  subrg1  20043  lsmsp  20357  lspprabs  20366  lsmcv  20412  psr1  21190  mat1  21605  lmcn2  22809  dvdsq1p  25334  wilthlem2  26227  dchr1  26414  ismir  27029  vdgfrgrgt2  28671  atcvatlem  30756  ressprs  31250  rngurd  31491  zarclssn  31832  ordtconnlem1  31883  cvmliftphtlem  33288  cvmlift3lem6  33295  cvmlift3lem9  33298  poimirlem13  35799  poimirlem14  35800  lsatexch  37064  lsatcvatlem  37070  oldmm1  37238  olj01  37246  olm01  37257  cvrcmp  37304  atcvreq0  37335  cvlexchb1  37351  cvlcvr1  37360  exatleN  37425  hlrelat3  37433  cvrval3  37434  cvratlem  37442  atlelt  37459  cvrat3  37463  2atjm  37466  atbtwn  37467  hlatexch3N  37501  hlatexch4  37502  2llnmat  37545  2atm  37548  lplnexllnN  37585  2llnjaN  37587  4atlem11b  37629  4atlem12b  37632  2lplnja  37640  dalem1  37680  dalemcea  37681  dalem3  37685  dalem8  37691  dalem16  37700  dalem17  37701  dalem21  37715  dalem25  37719  dalem39  37732  dalem54  37747  dalem55  37748  dalem57  37750  dalem60  37753  2lnat  37805  2atm2atN  37806  2llnma1b  37807  cdlema1N  37812  paddasslem12  37852  paddasslem13  37853  pmodlem1  37867  dalawlem2  37893  dalawlem3  37894  dalawlem5  37896  dalawlem6  37897  dalawlem8  37899  dalawlem11  37902  dalawlem12  37903  osumcllem1N  37977  lhp2lt  38022  lhpexle2lem  38030  lhpexle3lem  38032  lhpocnle  38037  lhpat3  38067  4atexlemtlw  38088  4atexlemnclw  38091  4atexlemcnd  38093  lautj  38114  lautm  38115  trlval3  38208  cdlemc5  38216  cdlemd3  38221  cdleme3g  38255  cdleme3h  38256  cdleme7d  38267  cdleme11c  38282  cdleme11k  38289  cdleme15d  38298  cdleme16e  38303  cdleme16f  38304  cdleme17b  38308  cdlemednpq  38320  cdleme19a  38324  cdleme20j  38339  cdleme21c  38348  cdleme22aa  38360  cdleme22b  38362  cdleme22cN  38363  cdleme22d  38364  cdleme23c  38372  cdleme28a  38391  cdleme35a  38469  cdleme35b  38471  cdleme35f  38475  cdleme42i  38504  cdlemeg46req  38550  cdlemf2  38583  cdlemg4c  38633  cdlemg6c  38641  cdlemg8b  38649  cdlemg10  38662  cdlemg11b  38663  cdlemg12f  38669  cdlemg13a  38672  cdlemg17a  38682  cdlemg17dALTN  38685  cdlemg18b  38700  cdlemg19a  38704  cdlemg27a  38713  cdlemg33b0  38722  cdlemg35  38734  cdlemg42  38750  cdlemg46  38756  trljco  38761  tendopltp  38801  cdlemi  38841  cdlemk3  38854  cdlemk10  38864  cdlemk15  38876  cdlemk1u  38880  cdlemk39  38937  cdlemk50  38973  erng1lem  39008  erngdvlem4  39012  erngdvlem4-rN  39020  dialss  39067  dia2dimlem1  39085  dia2dimlem10  39094  dia2dimlem12  39096  cdlemm10N  39139  djajN  39158  diblss  39191  cdlemn2  39216  dihjustlem  39237  dihord1  39239  dihord2pre2  39247  dib2dim  39264  dih2dimb  39265  dih2dimbALTN  39266  dihopelvalcpre  39269  dihord5b  39280  dihord5apre  39283  dihmeetlem1N  39311  dihglblem5apreN  39312  dihglblem2N  39315  dihmeetlem2N  39320  dihmeetlem3N  39326  lclkrlem2f  39533  lclkrlem2v  39549  lclkrslem2  39559  lcfrlem25  39588  lcfrlem35  39598  mapdlsm  39685  evlsval3  40279  numdenexp  40344  disjinfi  42738  fourierdlem54  43708  fourierdlem76  43730