Theorem mpbi2and 725

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  supiso  9471  hartogslem1  9539  cantnfp1lem3  9684  oemapwe  9698  cantnffval2  9699  mulne0d  11971  flflp1  13950  flval2  13957  remim  15289  ntrivcvgtail  16074  divalgmod  16581  divnumden  16929  numdensq  16935  numdenexp  16942  prmdivdiv  16969  4sqlem7  17127  isposd  18501  poslubmo  18588  posglbmo  18589  latasymd  18624  latjidm  18641  latmidm  18653  latledi  18656  latjass  18662  mod1ile  18672  isglbd  18688  lubun  18694  ismgmid2  18854  idressid  18867  oppginv  19578  slwhash  19843  lsmmod  19894  iscmnd  20013  dprd2da  20263  dmdprdsplit2lem  20266  dprdsplit  20269  pgpfac1lem1  20295  ringurd  20416  imasring  20565  subrg1  20839  isdrngd  21027  isdrngdOLD  21029  lsmsp  21366  lspprabs  21375  lsmcv  21424  psr1  22283  evlsval3  22403  mat1  22767  lmcn2  23973  dvdsq1p  26486  wilthlem2  27401  dchr1  27589  ismir  29136  vdgfrgrgt2  30904  atcvatlem  32992  ressprs  33573  rprmasso  34103  rprmasso3  34105  zarclssn  34551  ordtconnlem1  34602  cvmliftphtlem  36168  cvmlift3lem6  36175  cvmlift3lem9  36178  poimirlem13  38644  poimirlem14  38645  lsatexch  40193  lsatcvatlem  40199  oldmm1  40367  olj01  40375  olm01  40386  cvrcmp  40433  atcvreq0  40464  cvlexchb1  40480  cvlcvr1  40489  exatleN  40554  hlrelat3  40562  cvrval3  40563  cvratlem  40571  atlelt  40588  cvrat3  40592  2atjm  40595  atbtwn  40596  hlatexch3N  40630  hlatexch4  40631  2llnmat  40674  2atm  40677  lplnexllnN  40714  2llnjaN  40716  4atlem11b  40758  4atlem12b  40761  2lplnja  40769  dalem1  40809  dalemcea  40810  dalem3  40814  dalem8  40820  dalem16  40829  dalem17  40830  dalem21  40844  dalem25  40848  dalem39  40861  dalem54  40876  dalem55  40877  dalem57  40879  dalem60  40882  2lnat  40934  2atm2atN  40935  2llnma1b  40936  cdlema1N  40941  paddasslem12  40981  paddasslem13  40982  pmodlem1  40996  dalawlem2  41022  dalawlem3  41023  dalawlem5  41025  dalawlem6  41026  dalawlem8  41028  dalawlem11  41031  dalawlem12  41032  osumcllem1N  41106  lhp2lt  41151  lhpexle2lem  41159  lhpexle3lem  41161  lhpocnle  41166  lhpat3  41196  4atexlemtlw  41217  4atexlemnclw  41220  4atexlemcnd  41222  lautj  41243  lautm  41244  trlval3  41337  cdlemc5  41345  cdlemd3  41350  cdleme3g  41384  cdleme3h  41385  cdleme7d  41396  cdleme11c  41411  cdleme11k  41418  cdleme15d  41427  cdleme16e  41432  cdleme16f  41433  cdleme17b  41437  cdlemednpq  41449  cdleme19a  41453  cdleme20j  41468  cdleme21c  41477  cdleme22aa  41489  cdleme22b  41491  cdleme22cN  41492  cdleme22d  41493  cdleme23c  41501  cdleme28a  41520  cdleme35a  41598  cdleme35b  41600  cdleme35f  41604  cdleme42i  41633  cdlemeg46req  41679  cdlemf2  41712  cdlemg4c  41762  cdlemg6c  41770  cdlemg8b  41778  cdlemg10  41791  cdlemg11b  41792  cdlemg12f  41798  cdlemg13a  41801  cdlemg17a  41811  cdlemg17dALTN  41814  cdlemg18b  41829  cdlemg19a  41833  cdlemg27a  41842  cdlemg33b0  41851  cdlemg35  41863  cdlemg42  41879  cdlemg46  41885  trljco  41890  tendopltp  41930  cdlemi  41970  cdlemk3  41983  cdlemk10  41993  cdlemk15  42005  cdlemk1u  42009  cdlemk39  42066  cdlemk50  42102  erng1lem  42137  erngdvlem4  42141  erngdvlem4-rN  42149  dialss  42196  dia2dimlem1  42214  dia2dimlem10  42223  dia2dimlem12  42225  cdlemm10N  42268  djajN  42287  diblss  42320  cdlemn2  42345  dihjustlem  42366  dihord1  42368  dihord2pre2  42376  dib2dim  42393  dih2dimb  42394  dih2dimbALTN  42395  dihopelvalcpre  42398  dihord5b  42409  dihord5apre  42412  dihmeetlem1N  42440  dihglblem5apreN  42441  dihglblem2N  42444  dihmeetlem2N  42449  dihmeetlem3N  42455  lclkrlem2f  42662  lclkrlem2v  42678  lclkrslem2  42688  lcfrlem25  42717  lcfrlem35  42727  mapdlsm  42814  disjinfi  46300  fourierdlem54  47263  fourierdlem76  47285  uhgrimisgrgriclem  49121