Theorem mpbi2and 956

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  supiso  8381  hartogslem1  8447  cantnfp1lem3  8577  oemapwe  8591  cantnffval2  8592  mulne0d  10679  flflp1  12608  flval2  12615  remim  13857  ntrivcvgtail  14632  divalgmod  15129  divalgmodOLD  15130  divnumden  15456  numdensq  15462  prmdivdiv  15492  4sqlem7  15648  isposd  16955  latasymd  17057  latjidm  17074  latmidm  17086  latledi  17089  latjass  17095  mod1ile  17105  isglbd  17117  lubun  17123  poslubmo  17146  posglbmo  17147  ismgmid2  17267  oppginv  17789  slwhash  18039  lsmmod  18088  iscmnd  18205  dprd2da  18441  dmdprdsplit2lem  18444  dprdsplit  18447  pgpfac1lem1  18473  imasring  18619  isdrngd  18772  subrg1  18790  lsmsp  19086  lspprabs  19095  lsmcv  19141  psr1  19412  mat1  20253  topgele  20734  lmcn2  21452  dvdsq1p  23920  wilthlem2  24795  dchr1  24982  ismir  25554  vdgfrgrgt2  27162  atcvatlem  29244  ressprs  29655  rngurd  29788  ordtconnlem1  29970  cvmliftphtlem  31299  cvmlift3lem6  31306  cvmlift3lem9  31309  poimirlem13  33422  poimirlem14  33423  lsatexch  34330  lsatcvatlem  34336  oldmm1  34504  olj01  34512  olm01  34523  cvrcmp  34570  atcvreq0  34601  cvlexchb1  34617  cvlcvr1  34626  exatleN  34690  hlrelat3  34698  cvrval3  34699  cvratlem  34707  atlelt  34724  cvrat3  34728  2atjm  34731  atbtwn  34732  hlatexch3N  34766  hlatexch4  34767  2llnmat  34810  2atm  34813  lplnexllnN  34850  2llnjaN  34852  4atlem11b  34894  4atlem12b  34897  2lplnja  34905  dalem1  34945  dalemcea  34946  dalem3  34950  dalem8  34956  dalem16  34965  dalem17  34966  dalem21  34980  dalem25  34984  dalem39  34997  dalem54  35012  dalem55  35013  dalem57  35015  dalem60  35018  2lnat  35070  2atm2atN  35071  2llnma1b  35072  cdlema1N  35077  paddasslem12  35117  paddasslem13  35118  pmodlem1  35132  dalawlem2  35158  dalawlem3  35159  dalawlem5  35161  dalawlem6  35162  dalawlem8  35164  dalawlem11  35167  dalawlem12  35168  osumcllem1N  35242  lhp2lt  35287  lhpexle2lem  35295  lhpexle3lem  35297  lhpocnle  35302  lhpat3  35332  4atexlemtlw  35353  4atexlemnclw  35356  4atexlemcnd  35358  lautj  35379  lautm  35380  trlval3  35474  cdlemc5  35482  cdlemd3  35487  cdleme3g  35521  cdleme3h  35522  cdleme7d  35533  cdleme11c  35548  cdleme11k  35555  cdleme15d  35564  cdleme16e  35569  cdleme16f  35570  cdleme17b  35574  cdlemednpq  35586  cdleme19a  35591  cdleme20j  35606  cdleme21c  35615  cdleme22aa  35627  cdleme22b  35629  cdleme22cN  35630  cdleme22d  35631  cdleme23c  35639  cdleme28a  35658  cdleme35a  35736  cdleme35b  35738  cdleme35f  35742  cdleme42i  35771  cdlemeg46req  35817  cdlemf2  35850  cdlemg4c  35900  cdlemg6c  35908  cdlemg8b  35916  cdlemg10  35929  cdlemg11b  35930  cdlemg12f  35936  cdlemg13a  35939  cdlemg17a  35949  cdlemg17dALTN  35952  cdlemg18b  35967  cdlemg19a  35971  cdlemg27a  35980  cdlemg33b0  35989  cdlemg35  36001  cdlemg42  36017  cdlemg46  36023  trljco  36028  tendopltp  36068  cdlemi  36108  cdlemk3  36121  cdlemk10  36131  cdlemk15  36143  cdlemk1u  36147  cdlemk39  36204  cdlemk50  36240  erng1lem  36275  erngdvlem4  36279  erngdvlem4-rN  36287  dialss  36335  dia2dimlem1  36353  dia2dimlem10  36362  dia2dimlem12  36364  cdlemm10N  36407  djajN  36426  diblss  36459  cdlemn2  36484  dihjustlem  36505  dihord1  36507  dihord2pre2  36515  dib2dim  36532  dih2dimb  36533  dih2dimbALTN  36534  dihopelvalcpre  36537  dihord5b  36548  dihord5apre  36551  dihmeetlem1N  36579  dihglblem5apreN  36580  dihglblem2N  36583  dihmeetlem2N  36588  dihmeetlem3N  36594  lclkrlem2f  36801  lclkrlem2v  36817  lclkrslem2  36827  lcfrlem25  36856  lcfrlem35  36866  mapdlsm  36953  fourierdlem54  40377  fourierdlem76  40399