Theorem mpbi2and 958

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  supiso  8264  hartogslem1  8330  cantnfp1lem3  8460  oemapwe  8474  cantnffval2  8475  mulne0d  10558  flflp1  12470  flval2  12477  remim  13705  ntrivcvgtail  14471  divalgmod  14967  divalgmodOLD  14968  divnumden  15294  numdensq  15300  prmdivdiv  15330  4sqlem7  15486  isposd  16778  latasymd  16880  latjidm  16897  latmidm  16909  latledi  16912  latjass  16918  mod1ile  16928  isglbd  16940  lubun  16946  poslubmo  16969  posglbmo  16970  ismgmid2  17090  oppginv  17612  slwhash  17862  lsmmod  17911  iscmnd  18028  dprd2da  18264  dmdprdsplit2lem  18267  dprdsplit  18270  pgpfac1lem1  18296  imasring  18442  isdrngd  18595  subrg1  18613  lsmsp  18907  lspprabs  18916  lsmcv  18962  psr1  19233  mat1  20072  topgele  20549  lmcn2  21262  dvdsq1p  23724  wilthlem2  24595  dchr1  24782  ismir  25354  atcvatlem  28628  ressprs  28986  rngurd  29119  ordtconlem1  29298  cvmliftphtlem  30553  cvmlift3lem6  30560  cvmlift3lem9  30563  poimirlem13  32592  poimirlem14  32593  lsatexch  33348  lsatcvatlem  33354  oldmm1  33522  olj01  33530  olm01  33541  cvrcmp  33588  atcvreq0  33619  cvlexchb1  33635  cvlcvr1  33644  exatleN  33708  hlrelat3  33716  cvrval3  33717  cvratlem  33725  atlelt  33742  cvrat3  33746  2atjm  33749  atbtwn  33750  hlatexch3N  33784  hlatexch4  33785  2llnmat  33828  2atm  33831  lplnexllnN  33868  2llnjaN  33870  4atlem11b  33912  4atlem12b  33915  2lplnja  33923  dalem1  33963  dalemcea  33964  dalem3  33968  dalem8  33974  dalem16  33983  dalem17  33984  dalem21  33998  dalem25  34002  dalem39  34015  dalem54  34030  dalem55  34031  dalem57  34033  dalem60  34036  2lnat  34088  2atm2atN  34089  2llnma1b  34090  cdlema1N  34095  paddasslem12  34135  paddasslem13  34136  pmodlem1  34150  dalawlem2  34176  dalawlem3  34177  dalawlem5  34179  dalawlem6  34180  dalawlem8  34182  dalawlem11  34185  dalawlem12  34186  osumcllem1N  34260  lhp2lt  34305  lhpexle2lem  34313  lhpexle3lem  34315  lhpocnle  34320  lhpat3  34350  4atexlemtlw  34371  4atexlemnclw  34374  4atexlemcnd  34376  lautj  34397  lautm  34398  trlval3  34492  cdlemc5  34500  cdlemd3  34505  cdleme3g  34539  cdleme3h  34540  cdleme7d  34551  cdleme11c  34566  cdleme11k  34573  cdleme15d  34582  cdleme16e  34587  cdleme16f  34588  cdleme17b  34592  cdlemednpq  34604  cdleme19a  34609  cdleme20j  34624  cdleme21c  34633  cdleme22aa  34645  cdleme22b  34647  cdleme22cN  34648  cdleme22d  34649  cdleme23c  34657  cdleme28a  34676  cdleme35a  34754  cdleme35b  34756  cdleme35f  34760  cdleme42i  34789  cdlemeg46req  34835  cdlemf2  34868  cdlemg4c  34918  cdlemg6c  34926  cdlemg8b  34934  cdlemg10  34947  cdlemg11b  34948  cdlemg12f  34954  cdlemg13a  34957  cdlemg17a  34967  cdlemg17dALTN  34970  cdlemg18b  34985  cdlemg19a  34989  cdlemg27a  34998  cdlemg33b0  35007  cdlemg35  35019  cdlemg42  35035  cdlemg46  35041  trljco  35046  tendopltp  35086  cdlemi  35126  cdlemk3  35139  cdlemk10  35149  cdlemk15  35161  cdlemk1u  35165  cdlemk39  35222  cdlemk50  35258  erng1lem  35293  erngdvlem4  35297  erngdvlem4-rN  35305  dialss  35353  dia2dimlem1  35371  dia2dimlem10  35380  dia2dimlem12  35382  cdlemm10N  35425  djajN  35444  diblss  35477  cdlemn2  35502  dihjustlem  35523  dihord1  35525  dihord2pre2  35533  dib2dim  35550  dih2dimb  35551  dih2dimbALTN  35552  dihopelvalcpre  35555  dihord5b  35566  dihord5apre  35569  dihmeetlem1N  35597  dihglblem5apreN  35598  dihglblem2N  35601  dihmeetlem2N  35606  dihmeetlem3N  35612  lclkrlem2f  35819  lclkrlem2v  35835  lclkrslem2  35845  lcfrlem25  35874  lcfrlem35  35884  mapdlsm  35971  fourierdlem54  39053  fourierdlem76  39075  vdgfrgrgt2  41468