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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  supiso  9473  hartogslem1  9540  cantnfp1lem3  9678  oemapwe  9692  cantnffval2  9693  mulne0d  11871  flflp1  13777  flval2  13784  remim  15069  ntrivcvgtail  15851  divalgmod  16354  divnumden  16689  numdensq  16695  prmdivdiv  16725  4sqlem7  16882  isposd  18281  poslubmo  18369  posglbmo  18370  latasymd  18403  latjidm  18420  latmidm  18432  latledi  18435  latjass  18441  mod1ile  18451  isglbd  18467  lubun  18473  ismgmid2  18594  oppginv  19268  slwhash  19534  lsmmod  19585  iscmnd  19704  dprd2da  19954  dmdprdsplit2lem  19957  dprdsplit  19960  pgpfac1lem1  19986  ringurd  20080  imasring  20219  subrg1  20473  isdrngd  20534  isdrngdOLD  20536  lsmsp  20842  lspprabs  20851  lsmcv  20900  psr1  21752  mat1  22170  lmcn2  23374  dvdsq1p  25914  wilthlem2  26810  dchr1  26997  ismir  28178  vdgfrgrgt2  29819  atcvatlem  31906  ressprs  32401  zarclssn  33152  ordtconnlem1  33203  cvmliftphtlem  34607  cvmlift3lem6  34614  cvmlift3lem9  34617  poimirlem13  36805  poimirlem14  36806  lsatexch  38217  lsatcvatlem  38223  oldmm1  38391  olj01  38399  olm01  38410  cvrcmp  38457  atcvreq0  38488  cvlexchb1  38504  cvlcvr1  38513  exatleN  38579  hlrelat3  38587  cvrval3  38588  cvratlem  38596  atlelt  38613  cvrat3  38617  2atjm  38620  atbtwn  38621  hlatexch3N  38655  hlatexch4  38656  2llnmat  38699  2atm  38702  lplnexllnN  38739  2llnjaN  38741  4atlem11b  38783  4atlem12b  38786  2lplnja  38794  dalem1  38834  dalemcea  38835  dalem3  38839  dalem8  38845  dalem16  38854  dalem17  38855  dalem21  38869  dalem25  38873  dalem39  38886  dalem54  38901  dalem55  38902  dalem57  38904  dalem60  38907  2lnat  38959  2atm2atN  38960  2llnma1b  38961  cdlema1N  38966  paddasslem12  39006  paddasslem13  39007  pmodlem1  39021  dalawlem2  39047  dalawlem3  39048  dalawlem5  39050  dalawlem6  39051  dalawlem8  39053  dalawlem11  39056  dalawlem12  39057  osumcllem1N  39131  lhp2lt  39176  lhpexle2lem  39184  lhpexle3lem  39186  lhpocnle  39191  lhpat3  39221  4atexlemtlw  39242  4atexlemnclw  39245  4atexlemcnd  39247  lautj  39268  lautm  39269  trlval3  39362  cdlemc5  39370  cdlemd3  39375  cdleme3g  39409  cdleme3h  39410  cdleme7d  39421  cdleme11c  39436  cdleme11k  39443  cdleme15d  39452  cdleme16e  39457  cdleme16f  39458  cdleme17b  39462  cdlemednpq  39474  cdleme19a  39478  cdleme20j  39493  cdleme21c  39502  cdleme22aa  39514  cdleme22b  39516  cdleme22cN  39517  cdleme22d  39518  cdleme23c  39526  cdleme28a  39545  cdleme35a  39623  cdleme35b  39625  cdleme35f  39629  cdleme42i  39658  cdlemeg46req  39704  cdlemf2  39737  cdlemg4c  39787  cdlemg6c  39795  cdlemg8b  39803  cdlemg10  39816  cdlemg11b  39817  cdlemg12f  39823  cdlemg13a  39826  cdlemg17a  39836  cdlemg17dALTN  39839  cdlemg18b  39854  cdlemg19a  39858  cdlemg27a  39867  cdlemg33b0  39876  cdlemg35  39888  cdlemg42  39904  cdlemg46  39910  trljco  39915  tendopltp  39955  cdlemi  39995  cdlemk3  40008  cdlemk10  40018  cdlemk15  40030  cdlemk1u  40034  cdlemk39  40091  cdlemk50  40127  erng1lem  40162  erngdvlem4  40166  erngdvlem4-rN  40174  dialss  40221  dia2dimlem1  40239  dia2dimlem10  40248  dia2dimlem12  40250  cdlemm10N  40293  djajN  40312  diblss  40345  cdlemn2  40370  dihjustlem  40391  dihord1  40393  dihord2pre2  40401  dib2dim  40418  dih2dimb  40419  dih2dimbALTN  40420  dihopelvalcpre  40423  dihord5b  40434  dihord5apre  40437  dihmeetlem1N  40465  dihglblem5apreN  40466  dihglblem2N  40469  dihmeetlem2N  40474  dihmeetlem3N  40480  lclkrlem2f  40687  lclkrlem2v  40703  lclkrslem2  40713  lcfrlem25  40742  lcfrlem35  40752  mapdlsm  40839  evlsval3  41434  numdenexp  41531  disjinfi  44190  fourierdlem54  45175  fourierdlem76  45197