Theorem mpbi2and 710

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  supiso  8939  hartogslem1  9006  cantnfp1lem3  9143  oemapwe  9157  cantnffval2  9158  mulne0d  11292  flflp1  13178  flval2  13185  remim  14476  ntrivcvgtail  15256  divalgmod  15757  divnumden  16088  numdensq  16094  prmdivdiv  16124  4sqlem7  16280  isposd  17565  latasymd  17667  latjidm  17684  latmidm  17696  latledi  17699  latjass  17705  mod1ile  17715  isglbd  17727  lubun  17733  poslubmo  17756  posglbmo  17757  ismgmid2  17878  oppginv  18487  slwhash  18749  lsmmod  18801  iscmnd  18919  dprd2da  19164  dmdprdsplit2lem  19167  dprdsplit  19170  pgpfac1lem1  19196  imasring  19369  isdrngd  19527  subrg1  19545  lsmsp  19858  lspprabs  19867  lsmcv  19913  psr1  20192  mat1  21056  lmcn2  22257  dvdsq1p  24754  wilthlem2  25646  dchr1  25833  ismir  26445  vdgfrgrgt2  28077  atcvatlem  30162  ressprs  30642  rngurd  30857  ordtconnlem1  31167  cvmliftphtlem  32564  cvmlift3lem6  32571  cvmlift3lem9  32574  poimirlem13  34920  poimirlem14  34921  lsatexch  36194  lsatcvatlem  36200  oldmm1  36368  olj01  36376  olm01  36387  cvrcmp  36434  atcvreq0  36465  cvlexchb1  36481  cvlcvr1  36490  exatleN  36555  hlrelat3  36563  cvrval3  36564  cvratlem  36572  atlelt  36589  cvrat3  36593  2atjm  36596  atbtwn  36597  hlatexch3N  36631  hlatexch4  36632  2llnmat  36675  2atm  36678  lplnexllnN  36715  2llnjaN  36717  4atlem11b  36759  4atlem12b  36762  2lplnja  36770  dalem1  36810  dalemcea  36811  dalem3  36815  dalem8  36821  dalem16  36830  dalem17  36831  dalem21  36845  dalem25  36849  dalem39  36862  dalem54  36877  dalem55  36878  dalem57  36880  dalem60  36883  2lnat  36935  2atm2atN  36936  2llnma1b  36937  cdlema1N  36942  paddasslem12  36982  paddasslem13  36983  pmodlem1  36997  dalawlem2  37023  dalawlem3  37024  dalawlem5  37026  dalawlem6  37027  dalawlem8  37029  dalawlem11  37032  dalawlem12  37033  osumcllem1N  37107  lhp2lt  37152  lhpexle2lem  37160  lhpexle3lem  37162  lhpocnle  37167  lhpat3  37197  4atexlemtlw  37218  4atexlemnclw  37221  4atexlemcnd  37223  lautj  37244  lautm  37245  trlval3  37338  cdlemc5  37346  cdlemd3  37351  cdleme3g  37385  cdleme3h  37386  cdleme7d  37397  cdleme11c  37412  cdleme11k  37419  cdleme15d  37428  cdleme16e  37433  cdleme16f  37434  cdleme17b  37438  cdlemednpq  37450  cdleme19a  37454  cdleme20j  37469  cdleme21c  37478  cdleme22aa  37490  cdleme22b  37492  cdleme22cN  37493  cdleme22d  37494  cdleme23c  37502  cdleme28a  37521  cdleme35a  37599  cdleme35b  37601  cdleme35f  37605  cdleme42i  37634  cdlemeg46req  37680  cdlemf2  37713  cdlemg4c  37763  cdlemg6c  37771  cdlemg8b  37779  cdlemg10  37792  cdlemg11b  37793  cdlemg12f  37799  cdlemg13a  37802  cdlemg17a  37812  cdlemg17dALTN  37815  cdlemg18b  37830  cdlemg19a  37834  cdlemg27a  37843  cdlemg33b0  37852  cdlemg35  37864  cdlemg42  37880  cdlemg46  37886  trljco  37891  tendopltp  37931  cdlemi  37971  cdlemk3  37984  cdlemk10  37994  cdlemk15  38006  cdlemk1u  38010  cdlemk39  38067  cdlemk50  38103  erng1lem  38138  erngdvlem4  38142  erngdvlem4-rN  38150  dialss  38197  dia2dimlem1  38215  dia2dimlem10  38224  dia2dimlem12  38226  cdlemm10N  38269  djajN  38288  diblss  38321  cdlemn2  38346  dihjustlem  38367  dihord1  38369  dihord2pre2  38377  dib2dim  38394  dih2dimb  38395  dih2dimbALTN  38396  dihopelvalcpre  38399  dihord5b  38410  dihord5apre  38413  dihmeetlem1N  38441  dihglblem5apreN  38442  dihglblem2N  38445  dihmeetlem2N  38450  dihmeetlem3N  38456  lclkrlem2f  38663  lclkrlem2v  38679  lclkrslem2  38689  lcfrlem25  38718  lcfrlem35  38728  mapdlsm  38815  numdenexp  39235  fourierdlem54  42494  fourierdlem76  42516