Theorem mpbi2and 712

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  supiso  9012  hartogslem1  9079  cantnfp1lem3  9216  oemapwe  9230  cantnffval2  9231  mulne0d  11370  flflp1  13268  flval2  13275  remim  14566  ntrivcvgtail  15348  divalgmod  15851  divnumden  16188  numdensq  16194  prmdivdiv  16224  4sqlem7  16380  isposd  17681  latasymd  17783  latjidm  17800  latmidm  17812  latledi  17815  latjass  17821  mod1ile  17831  isglbd  17843  lubun  17849  poslubmo  17872  posglbmo  17873  ismgmid2  17994  oppginv  18605  slwhash  18867  lsmmod  18919  iscmnd  19037  dprd2da  19283  dmdprdsplit2lem  19286  dprdsplit  19289  pgpfac1lem1  19315  imasring  19491  isdrngd  19646  subrg1  19664  lsmsp  19977  lspprabs  19986  lsmcv  20032  psr1  20791  mat1  21198  lmcn2  22400  dvdsq1p  24913  wilthlem2  25806  dchr1  25993  ismir  26605  vdgfrgrgt2  28235  atcvatlem  30320  ressprs  30815  rngurd  31059  zarclssn  31395  ordtconnlem1  31446  cvmliftphtlem  32850  cvmlift3lem6  32857  cvmlift3lem9  32860  poimirlem13  35413  poimirlem14  35414  lsatexch  36680  lsatcvatlem  36686  oldmm1  36854  olj01  36862  olm01  36873  cvrcmp  36920  atcvreq0  36951  cvlexchb1  36967  cvlcvr1  36976  exatleN  37041  hlrelat3  37049  cvrval3  37050  cvratlem  37058  atlelt  37075  cvrat3  37079  2atjm  37082  atbtwn  37083  hlatexch3N  37117  hlatexch4  37118  2llnmat  37161  2atm  37164  lplnexllnN  37201  2llnjaN  37203  4atlem11b  37245  4atlem12b  37248  2lplnja  37256  dalem1  37296  dalemcea  37297  dalem3  37301  dalem8  37307  dalem16  37316  dalem17  37317  dalem21  37331  dalem25  37335  dalem39  37348  dalem54  37363  dalem55  37364  dalem57  37366  dalem60  37369  2lnat  37421  2atm2atN  37422  2llnma1b  37423  cdlema1N  37428  paddasslem12  37468  paddasslem13  37469  pmodlem1  37483  dalawlem2  37509  dalawlem3  37510  dalawlem5  37512  dalawlem6  37513  dalawlem8  37515  dalawlem11  37518  dalawlem12  37519  osumcllem1N  37593  lhp2lt  37638  lhpexle2lem  37646  lhpexle3lem  37648  lhpocnle  37653  lhpat3  37683  4atexlemtlw  37704  4atexlemnclw  37707  4atexlemcnd  37709  lautj  37730  lautm  37731  trlval3  37824  cdlemc5  37832  cdlemd3  37837  cdleme3g  37871  cdleme3h  37872  cdleme7d  37883  cdleme11c  37898  cdleme11k  37905  cdleme15d  37914  cdleme16e  37919  cdleme16f  37920  cdleme17b  37924  cdlemednpq  37936  cdleme19a  37940  cdleme20j  37955  cdleme21c  37964  cdleme22aa  37976  cdleme22b  37978  cdleme22cN  37979  cdleme22d  37980  cdleme23c  37988  cdleme28a  38007  cdleme35a  38085  cdleme35b  38087  cdleme35f  38091  cdleme42i  38120  cdlemeg46req  38166  cdlemf2  38199  cdlemg4c  38249  cdlemg6c  38257  cdlemg8b  38265  cdlemg10  38278  cdlemg11b  38279  cdlemg12f  38285  cdlemg13a  38288  cdlemg17a  38298  cdlemg17dALTN  38301  cdlemg18b  38316  cdlemg19a  38320  cdlemg27a  38329  cdlemg33b0  38338  cdlemg35  38350  cdlemg42  38366  cdlemg46  38372  trljco  38377  tendopltp  38417  cdlemi  38457  cdlemk3  38470  cdlemk10  38480  cdlemk15  38492  cdlemk1u  38496  cdlemk39  38553  cdlemk50  38589  erng1lem  38624  erngdvlem4  38628  erngdvlem4-rN  38636  dialss  38683  dia2dimlem1  38701  dia2dimlem10  38710  dia2dimlem12  38712  cdlemm10N  38755  djajN  38774  diblss  38807  cdlemn2  38832  dihjustlem  38853  dihord1  38855  dihord2pre2  38863  dib2dim  38880  dih2dimb  38881  dih2dimbALTN  38882  dihopelvalcpre  38885  dihord5b  38896  dihord5apre  38899  dihmeetlem1N  38927  dihglblem5apreN  38928  dihglblem2N  38931  dihmeetlem2N  38936  dihmeetlem3N  38942  lclkrlem2f  39149  lclkrlem2v  39165  lclkrslem2  39175  lcfrlem25  39204  lcfrlem35  39214  mapdlsm  39301  evlsval3  39851  numdenexp  39914  disjinfi  42269  fourierdlem54  43243  fourierdlem76  43265