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  9450  hartogslem1  9518  cantnfp1lem3  9663  oemapwe  9677  cantnffval2  9678  mulne0d  11894  flflp1  13872  flval2  13879  remim  15208  ntrivcvgtail  15993  divalgmod  16502  divnumden  16845  numdensq  16851  numdenexp  16857  prmdivdiv  16884  4sqlem7  17042  isposd  18416  poslubmo  18503  posglbmo  18504  latasymd  18539  latjidm  18556  latmidm  18568  latledi  18571  latjass  18577  mod1ile  18587  isglbd  18603  lubun  18609  ismgmid2  18768  idressid  18781  oppginv  19492  slwhash  19757  lsmmod  19808  iscmnd  19927  dprd2da  20177  dmdprdsplit2lem  20180  dprdsplit  20183  pgpfac1lem1  20209  ringurd  20330  imasring  20477  subrg1  20750  isdrngd  20937  isdrngdOLD  20939  lsmsp  21276  lspprabs  21285  lsmcv  21334  psr1  22191  evlsval3  22311  mat1  22675  lmcn2  23881  dvdsq1p  26395  wilthlem2  27313  dchr1  27501  ismir  29018  vdgfrgrgt2  30786  atcvatlem  32874  ressprs  33414  rprmasso  33943  rprmasso3  33945  zarclssn  34391  ordtconnlem1  34442  cvmliftphtlem  35904  cvmlift3lem6  35911  cvmlift3lem9  35914  poimirlem13  38390  poimirlem14  38391  lsatexch  39924  lsatcvatlem  39930  oldmm1  40098  olj01  40106  olm01  40117  cvrcmp  40164  atcvreq0  40195  cvlexchb1  40211  cvlcvr1  40220  exatleN  40285  hlrelat3  40293  cvrval3  40294  cvratlem  40302  atlelt  40319  cvrat3  40323  2atjm  40326  atbtwn  40327  hlatexch3N  40361  hlatexch4  40362  2llnmat  40405  2atm  40408  lplnexllnN  40445  2llnjaN  40447  4atlem11b  40489  4atlem12b  40492  2lplnja  40500  dalem1  40540  dalemcea  40541  dalem3  40545  dalem8  40551  dalem16  40560  dalem17  40561  dalem21  40575  dalem25  40579  dalem39  40592  dalem54  40607  dalem55  40608  dalem57  40610  dalem60  40613  2lnat  40665  2atm2atN  40666  2llnma1b  40667  cdlema1N  40672  paddasslem12  40712  paddasslem13  40713  pmodlem1  40727  dalawlem2  40753  dalawlem3  40754  dalawlem5  40756  dalawlem6  40757  dalawlem8  40759  dalawlem11  40762  dalawlem12  40763  osumcllem1N  40837  lhp2lt  40882  lhpexle2lem  40890  lhpexle3lem  40892  lhpocnle  40897  lhpat3  40927  4atexlemtlw  40948  4atexlemnclw  40951  4atexlemcnd  40953  lautj  40974  lautm  40975  trlval3  41068  cdlemc5  41076  cdlemd3  41081  cdleme3g  41115  cdleme3h  41116  cdleme7d  41127  cdleme11c  41142  cdleme11k  41149  cdleme15d  41158  cdleme16e  41163  cdleme16f  41164  cdleme17b  41168  cdlemednpq  41180  cdleme19a  41184  cdleme20j  41199  cdleme21c  41208  cdleme22aa  41220  cdleme22b  41222  cdleme22cN  41223  cdleme22d  41224  cdleme23c  41232  cdleme28a  41251  cdleme35a  41329  cdleme35b  41331  cdleme35f  41335  cdleme42i  41364  cdlemeg46req  41410  cdlemf2  41443  cdlemg4c  41493  cdlemg6c  41501  cdlemg8b  41509  cdlemg10  41522  cdlemg11b  41523  cdlemg12f  41529  cdlemg13a  41532  cdlemg17a  41542  cdlemg17dALTN  41545  cdlemg18b  41560  cdlemg19a  41564  cdlemg27a  41573  cdlemg33b0  41582  cdlemg35  41594  cdlemg42  41610  cdlemg46  41616  trljco  41621  tendopltp  41661  cdlemi  41701  cdlemk3  41714  cdlemk10  41724  cdlemk15  41736  cdlemk1u  41740  cdlemk39  41797  cdlemk50  41833  erng1lem  41868  erngdvlem4  41872  erngdvlem4-rN  41880  dialss  41927  dia2dimlem1  41945  dia2dimlem10  41954  dia2dimlem12  41956  cdlemm10N  41999  djajN  42018  diblss  42051  cdlemn2  42076  dihjustlem  42097  dihord1  42099  dihord2pre2  42107  dib2dim  42124  dih2dimb  42125  dih2dimbALTN  42126  dihopelvalcpre  42129  dihord5b  42140  dihord5apre  42143  dihmeetlem1N  42171  dihglblem5apreN  42172  dihglblem2N  42175  dihmeetlem2N  42180  dihmeetlem3N  42186  lclkrlem2f  42393  lclkrlem2v  42409  lclkrslem2  42419  lcfrlem25  42448  lcfrlem35  42458  mapdlsm  42545  disjinfi  46032  fourierdlem54  46996  fourierdlem76  47018  uhgrimisgrgriclem  48854