Theorem mpbi2and 710

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  9466  hartogslem1  9533  cantnfp1lem3  9671  oemapwe  9685  cantnffval2  9686  mulne0d  11862  flflp1  13768  flval2  13775  remim  15060  ntrivcvgtail  15842  divalgmod  16345  divnumden  16680  numdensq  16686  prmdivdiv  16716  4sqlem7  16873  isposd  18272  poslubmo  18360  posglbmo  18361  latasymd  18394  latjidm  18411  latmidm  18423  latledi  18426  latjass  18432  mod1ile  18442  isglbd  18458  lubun  18464  ismgmid2  18583  oppginv  19220  slwhash  19486  lsmmod  19537  iscmnd  19656  dprd2da  19906  dmdprdsplit2lem  19909  dprdsplit  19912  pgpfac1lem1  19938  imasring  20136  isdrngd  20340  isdrngdOLD  20342  subrg1  20365  lsmsp  20689  lspprabs  20698  lsmcv  20746  psr1  21523  mat1  21940  lmcn2  23144  dvdsq1p  25669  wilthlem2  26562  dchr1  26749  ismir  27899  vdgfrgrgt2  29540  atcvatlem  31625  ressprs  32120  rngurd  32367  zarclssn  32841  ordtconnlem1  32892  cvmliftphtlem  34296  cvmlift3lem6  34303  cvmlift3lem9  34306  poimirlem13  36489  poimirlem14  36490  lsatexch  37901  lsatcvatlem  37907  oldmm1  38075  olj01  38083  olm01  38094  cvrcmp  38141  atcvreq0  38172  cvlexchb1  38188  cvlcvr1  38197  exatleN  38263  hlrelat3  38271  cvrval3  38272  cvratlem  38280  atlelt  38297  cvrat3  38301  2atjm  38304  atbtwn  38305  hlatexch3N  38339  hlatexch4  38340  2llnmat  38383  2atm  38386  lplnexllnN  38423  2llnjaN  38425  4atlem11b  38467  4atlem12b  38470  2lplnja  38478  dalem1  38518  dalemcea  38519  dalem3  38523  dalem8  38529  dalem16  38538  dalem17  38539  dalem21  38553  dalem25  38557  dalem39  38570  dalem54  38585  dalem55  38586  dalem57  38588  dalem60  38591  2lnat  38643  2atm2atN  38644  2llnma1b  38645  cdlema1N  38650  paddasslem12  38690  paddasslem13  38691  pmodlem1  38705  dalawlem2  38731  dalawlem3  38732  dalawlem5  38734  dalawlem6  38735  dalawlem8  38737  dalawlem11  38740  dalawlem12  38741  osumcllem1N  38815  lhp2lt  38860  lhpexle2lem  38868  lhpexle3lem  38870  lhpocnle  38875  lhpat3  38905  4atexlemtlw  38926  4atexlemnclw  38929  4atexlemcnd  38931  lautj  38952  lautm  38953  trlval3  39046  cdlemc5  39054  cdlemd3  39059  cdleme3g  39093  cdleme3h  39094  cdleme7d  39105  cdleme11c  39120  cdleme11k  39127  cdleme15d  39136  cdleme16e  39141  cdleme16f  39142  cdleme17b  39146  cdlemednpq  39158  cdleme19a  39162  cdleme20j  39177  cdleme21c  39186  cdleme22aa  39198  cdleme22b  39200  cdleme22cN  39201  cdleme22d  39202  cdleme23c  39210  cdleme28a  39229  cdleme35a  39307  cdleme35b  39309  cdleme35f  39313  cdleme42i  39342  cdlemeg46req  39388  cdlemf2  39421  cdlemg4c  39471  cdlemg6c  39479  cdlemg8b  39487  cdlemg10  39500  cdlemg11b  39501  cdlemg12f  39507  cdlemg13a  39510  cdlemg17a  39520  cdlemg17dALTN  39523  cdlemg18b  39538  cdlemg19a  39542  cdlemg27a  39551  cdlemg33b0  39560  cdlemg35  39572  cdlemg42  39588  cdlemg46  39594  trljco  39599  tendopltp  39639  cdlemi  39679  cdlemk3  39692  cdlemk10  39702  cdlemk15  39714  cdlemk1u  39718  cdlemk39  39775  cdlemk50  39811  erng1lem  39846  erngdvlem4  39850  erngdvlem4-rN  39858  dialss  39905  dia2dimlem1  39923  dia2dimlem10  39932  dia2dimlem12  39934  cdlemm10N  39977  djajN  39996  diblss  40029  cdlemn2  40054  dihjustlem  40075  dihord1  40077  dihord2pre2  40085  dib2dim  40102  dih2dimb  40103  dih2dimbALTN  40104  dihopelvalcpre  40107  dihord5b  40118  dihord5apre  40121  dihmeetlem1N  40149  dihglblem5apreN  40150  dihglblem2N  40153  dihmeetlem2N  40158  dihmeetlem3N  40164  lclkrlem2f  40371  lclkrlem2v  40387  lclkrslem2  40397  lcfrlem25  40426  lcfrlem35  40436  mapdlsm  40523  evlsval3  41128  numdenexp  41223  disjinfi  43876  fourierdlem54  44862  fourierdlem76  44884