Theorem mpbi2and 713

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  supiso  9383  hartogslem1  9451  cantnfp1lem3  9593  oemapwe  9607  cantnffval2  9608  mulne0d  11793  flflp1  13731  flval2  13738  remim  15044  ntrivcvgtail  15827  divalgmod  16337  divnumden  16679  numdensq  16685  numdenexp  16691  prmdivdiv  16718  4sqlem7  16876  isposd  18249  poslubmo  18336  posglbmo  18337  latasymd  18372  latjidm  18389  latmidm  18401  latledi  18404  latjass  18410  mod1ile  18420  isglbd  18436  lubun  18442  ismgmid2  18597  oppginv  19292  slwhash  19557  lsmmod  19608  iscmnd  19727  dprd2da  19977  dmdprdsplit2lem  19980  dprdsplit  19983  pgpfac1lem1  20009  ringurd  20124  imasring  20270  subrg1  20519  isdrngd  20702  isdrngdOLD  20704  lsmsp  21042  lspprabs  21051  lsmcv  21100  psr1  21930  evlsval3  22048  mat1  22395  lmcn2  23597  dvdsq1p  26128  wilthlem2  27039  dchr1  27228  ismir  28714  vdgfrgrgt2  30356  atcvatlem  32443  ressprs  33029  rprmasso  33587  rprmasso3  33589  zarclssn  34011  ordtconnlem1  34062  cvmliftphtlem  35492  cvmlift3lem6  35499  cvmlift3lem9  35502  poimirlem13  37805  poimirlem14  37806  lsatexch  39340  lsatcvatlem  39346  oldmm1  39514  olj01  39522  olm01  39533  cvrcmp  39580  atcvreq0  39611  cvlexchb1  39627  cvlcvr1  39636  exatleN  39701  hlrelat3  39709  cvrval3  39710  cvratlem  39718  atlelt  39735  cvrat3  39739  2atjm  39742  atbtwn  39743  hlatexch3N  39777  hlatexch4  39778  2llnmat  39821  2atm  39824  lplnexllnN  39861  2llnjaN  39863  4atlem11b  39905  4atlem12b  39908  2lplnja  39916  dalem1  39956  dalemcea  39957  dalem3  39961  dalem8  39967  dalem16  39976  dalem17  39977  dalem21  39991  dalem25  39995  dalem39  40008  dalem54  40023  dalem55  40024  dalem57  40026  dalem60  40029  2lnat  40081  2atm2atN  40082  2llnma1b  40083  cdlema1N  40088  paddasslem12  40128  paddasslem13  40129  pmodlem1  40143  dalawlem2  40169  dalawlem3  40170  dalawlem5  40172  dalawlem6  40173  dalawlem8  40175  dalawlem11  40178  dalawlem12  40179  osumcllem1N  40253  lhp2lt  40298  lhpexle2lem  40306  lhpexle3lem  40308  lhpocnle  40313  lhpat3  40343  4atexlemtlw  40364  4atexlemnclw  40367  4atexlemcnd  40369  lautj  40390  lautm  40391  trlval3  40484  cdlemc5  40492  cdlemd3  40497  cdleme3g  40531  cdleme3h  40532  cdleme7d  40543  cdleme11c  40558  cdleme11k  40565  cdleme15d  40574  cdleme16e  40579  cdleme16f  40580  cdleme17b  40584  cdlemednpq  40596  cdleme19a  40600  cdleme20j  40615  cdleme21c  40624  cdleme22aa  40636  cdleme22b  40638  cdleme22cN  40639  cdleme22d  40640  cdleme23c  40648  cdleme28a  40667  cdleme35a  40745  cdleme35b  40747  cdleme35f  40751  cdleme42i  40780  cdlemeg46req  40826  cdlemf2  40859  cdlemg4c  40909  cdlemg6c  40917  cdlemg8b  40925  cdlemg10  40938  cdlemg11b  40939  cdlemg12f  40945  cdlemg13a  40948  cdlemg17a  40958  cdlemg17dALTN  40961  cdlemg18b  40976  cdlemg19a  40980  cdlemg27a  40989  cdlemg33b0  40998  cdlemg35  41010  cdlemg42  41026  cdlemg46  41032  trljco  41037  tendopltp  41077  cdlemi  41117  cdlemk3  41130  cdlemk10  41140  cdlemk15  41152  cdlemk1u  41156  cdlemk39  41213  cdlemk50  41249  erng1lem  41284  erngdvlem4  41288  erngdvlem4-rN  41296  dialss  41343  dia2dimlem1  41361  dia2dimlem10  41370  dia2dimlem12  41372  cdlemm10N  41415  djajN  41434  diblss  41467  cdlemn2  41492  dihjustlem  41513  dihord1  41515  dihord2pre2  41523  dib2dim  41540  dih2dimb  41541  dih2dimbALTN  41542  dihopelvalcpre  41545  dihord5b  41556  dihord5apre  41559  dihmeetlem1N  41587  dihglblem5apreN  41588  dihglblem2N  41591  dihmeetlem2N  41596  dihmeetlem3N  41602  lclkrlem2f  41809  lclkrlem2v  41825  lclkrslem2  41835  lcfrlem25  41864  lcfrlem35  41874  mapdlsm  41961  disjinfi  45472  fourierdlem54  46440  fourierdlem76  46462  uhgrimisgrgriclem  48212