Theorem mpbi2and 725

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  supiso  9495  hartogslem1  9563  cantnfp1lem3  9708  oemapwe  9722  cantnffval2  9723  mulne0d  11995  flflp1  13974  flval2  13981  remim  15313  ntrivcvgtail  16098  divalgmod  16605  divnumden  16953  numdensq  16959  numdenexp  16966  prmdivdiv  16993  4sqlem7  17151  isposd  18525  poslubmo  18612  posglbmo  18613  latasymd  18648  latjidm  18665  latmidm  18677  latledi  18680  latjass  18686  mod1ile  18696  isglbd  18712  lubun  18718  ismgmid2  18878  idressid  18891  oppginv  19603  slwhash  19868  lsmmod  19919  iscmnd  20038  dprd2da  20288  dmdprdsplit2lem  20291  dprdsplit  20294  pgpfac1lem1  20320  ringurd  20441  imasring  20590  subrg1  20864  isdrngd  21052  isdrngdOLD  21054  lsmsp  21391  lspprabs  21400  lsmcv  21449  psr1  22308  evlsval3  22428  mat1  22792  lmcn2  23998  dvdsq1p  26511  wilthlem2  27426  dchr1  27614  ismir  29161  vdgfrgrgt2  30929  atcvatlem  33017  ressprs  33597  rprmasso  34127  rprmasso3  34129  zarclssn  34575  ordtconnlem1  34626  cvmliftphtlem  36249  cvmlift3lem6  36256  cvmlift3lem9  36259  poimirlem13  38743  poimirlem14  38744  lsatexch  40292  lsatcvatlem  40298  oldmm1  40466  olj01  40474  olm01  40485  cvrcmp  40532  atcvreq0  40563  cvlexchb1  40579  cvlcvr1  40588  exatleN  40653  hlrelat3  40661  cvrval3  40662  cvratlem  40670  atlelt  40687  cvrat3  40691  2atjm  40694  atbtwn  40695  hlatexch3N  40729  hlatexch4  40730  2llnmat  40773  2atm  40776  lplnexllnN  40813  2llnjaN  40815  4atlem11b  40857  4atlem12b  40860  2lplnja  40868  dalem1  40908  dalemcea  40909  dalem3  40913  dalem8  40919  dalem16  40928  dalem17  40929  dalem21  40943  dalem25  40947  dalem39  40960  dalem54  40975  dalem55  40976  dalem57  40978  dalem60  40981  2lnat  41033  2atm2atN  41034  2llnma1b  41035  cdlema1N  41040  paddasslem12  41080  paddasslem13  41081  pmodlem1  41095  dalawlem2  41121  dalawlem3  41122  dalawlem5  41124  dalawlem6  41125  dalawlem8  41127  dalawlem11  41130  dalawlem12  41131  osumcllem1N  41205  lhp2lt  41250  lhpexle2lem  41258  lhpexle3lem  41260  lhpocnle  41265  lhpat3  41295  4atexlemtlw  41316  4atexlemnclw  41319  4atexlemcnd  41321  lautj  41342  lautm  41343  trlval3  41436  cdlemc5  41444  cdlemd3  41449  cdleme3g  41483  cdleme3h  41484  cdleme7d  41495  cdleme11c  41510  cdleme11k  41517  cdleme15d  41526  cdleme16e  41531  cdleme16f  41532  cdleme17b  41536  cdlemednpq  41548  cdleme19a  41552  cdleme20j  41567  cdleme21c  41576  cdleme22aa  41588  cdleme22b  41590  cdleme22cN  41591  cdleme22d  41592  cdleme23c  41600  cdleme28a  41619  cdleme35a  41697  cdleme35b  41699  cdleme35f  41703  cdleme42i  41732  cdlemeg46req  41778  cdlemf2  41811  cdlemg4c  41861  cdlemg6c  41869  cdlemg8b  41877  cdlemg10  41890  cdlemg11b  41891  cdlemg12f  41897  cdlemg13a  41900  cdlemg17a  41910  cdlemg17dALTN  41913  cdlemg18b  41928  cdlemg19a  41932  cdlemg27a  41941  cdlemg33b0  41950  cdlemg35  41962  cdlemg42  41978  cdlemg46  41984  trljco  41989  tendopltp  42029  cdlemi  42069  cdlemk3  42082  cdlemk10  42092  cdlemk15  42104  cdlemk1u  42108  cdlemk39  42165  cdlemk50  42201  erng1lem  42236  erngdvlem4  42240  erngdvlem4-rN  42248  dialss  42295  dia2dimlem1  42313  dia2dimlem10  42322  dia2dimlem12  42324  cdlemm10N  42367  djajN  42386  diblss  42419  cdlemn2  42444  dihjustlem  42465  dihord1  42467  dihord2pre2  42475  dib2dim  42492  dih2dimb  42493  dih2dimbALTN  42494  dihopelvalcpre  42497  dihord5b  42508  dihord5apre  42511  dihmeetlem1N  42539  dihglblem5apreN  42540  dihglblem2N  42543  dihmeetlem2N  42548  dihmeetlem3N  42554  lclkrlem2f  42761  lclkrlem2v  42777  lclkrslem2  42787  lcfrlem25  42816  lcfrlem35  42826  mapdlsm  42913  disjinfi  46412  fourierdlem54  47375  fourierdlem76  47397  uhgrimisgrgriclem  49233