Theorem mpbi2and 711

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  9544  hartogslem1  9611  cantnfp1lem3  9749  oemapwe  9763  cantnffval2  9764  mulne0d  11942  flflp1  13858  flval2  13865  remim  15166  ntrivcvgtail  15948  divalgmod  16454  divnumden  16795  numdensq  16801  numdenexp  16807  prmdivdiv  16834  4sqlem7  16991  isposd  18393  poslubmo  18481  posglbmo  18482  latasymd  18515  latjidm  18532  latmidm  18544  latledi  18547  latjass  18553  mod1ile  18563  isglbd  18579  lubun  18585  ismgmid2  18706  oppginv  19402  slwhash  19666  lsmmod  19717  iscmnd  19836  dprd2da  20086  dmdprdsplit2lem  20089  dprdsplit  20092  pgpfac1lem1  20118  ringurd  20212  imasring  20353  subrg1  20610  isdrngd  20787  isdrngdOLD  20789  lsmsp  21108  lspprabs  21117  lsmcv  21166  psr1  22014  mat1  22474  lmcn2  23678  dvdsq1p  26222  wilthlem2  27130  dchr1  27319  ismir  28685  vdgfrgrgt2  30330  atcvatlem  32417  ressprs  32936  rprmasso  33518  rprmasso3  33520  zarclssn  33819  ordtconnlem1  33870  cvmliftphtlem  35285  cvmlift3lem6  35292  cvmlift3lem9  35295  poimirlem13  37593  poimirlem14  37594  lsatexch  38999  lsatcvatlem  39005  oldmm1  39173  olj01  39181  olm01  39192  cvrcmp  39239  atcvreq0  39270  cvlexchb1  39286  cvlcvr1  39295  exatleN  39361  hlrelat3  39369  cvrval3  39370  cvratlem  39378  atlelt  39395  cvrat3  39399  2atjm  39402  atbtwn  39403  hlatexch3N  39437  hlatexch4  39438  2llnmat  39481  2atm  39484  lplnexllnN  39521  2llnjaN  39523  4atlem11b  39565  4atlem12b  39568  2lplnja  39576  dalem1  39616  dalemcea  39617  dalem3  39621  dalem8  39627  dalem16  39636  dalem17  39637  dalem21  39651  dalem25  39655  dalem39  39668  dalem54  39683  dalem55  39684  dalem57  39686  dalem60  39689  2lnat  39741  2atm2atN  39742  2llnma1b  39743  cdlema1N  39748  paddasslem12  39788  paddasslem13  39789  pmodlem1  39803  dalawlem2  39829  dalawlem3  39830  dalawlem5  39832  dalawlem6  39833  dalawlem8  39835  dalawlem11  39838  dalawlem12  39839  osumcllem1N  39913  lhp2lt  39958  lhpexle2lem  39966  lhpexle3lem  39968  lhpocnle  39973  lhpat3  40003  4atexlemtlw  40024  4atexlemnclw  40027  4atexlemcnd  40029  lautj  40050  lautm  40051  trlval3  40144  cdlemc5  40152  cdlemd3  40157  cdleme3g  40191  cdleme3h  40192  cdleme7d  40203  cdleme11c  40218  cdleme11k  40225  cdleme15d  40234  cdleme16e  40239  cdleme16f  40240  cdleme17b  40244  cdlemednpq  40256  cdleme19a  40260  cdleme20j  40275  cdleme21c  40284  cdleme22aa  40296  cdleme22b  40298  cdleme22cN  40299  cdleme22d  40300  cdleme23c  40308  cdleme28a  40327  cdleme35a  40405  cdleme35b  40407  cdleme35f  40411  cdleme42i  40440  cdlemeg46req  40486  cdlemf2  40519  cdlemg4c  40569  cdlemg6c  40577  cdlemg8b  40585  cdlemg10  40598  cdlemg11b  40599  cdlemg12f  40605  cdlemg13a  40608  cdlemg17a  40618  cdlemg17dALTN  40621  cdlemg18b  40636  cdlemg19a  40640  cdlemg27a  40649  cdlemg33b0  40658  cdlemg35  40670  cdlemg42  40686  cdlemg46  40692  trljco  40697  tendopltp  40737  cdlemi  40777  cdlemk3  40790  cdlemk10  40800  cdlemk15  40812  cdlemk1u  40816  cdlemk39  40873  cdlemk50  40909  erng1lem  40944  erngdvlem4  40948  erngdvlem4-rN  40956  dialss  41003  dia2dimlem1  41021  dia2dimlem10  41030  dia2dimlem12  41032  cdlemm10N  41075  djajN  41094  diblss  41127  cdlemn2  41152  dihjustlem  41173  dihord1  41175  dihord2pre2  41183  dib2dim  41200  dih2dimb  41201  dih2dimbALTN  41202  dihopelvalcpre  41205  dihord5b  41216  dihord5apre  41219  dihmeetlem1N  41247  dihglblem5apreN  41248  dihglblem2N  41251  dihmeetlem2N  41256  dihmeetlem3N  41262  lclkrlem2f  41469  lclkrlem2v  41485  lclkrslem2  41495  lcfrlem25  41524  lcfrlem35  41534  mapdlsm  41621  evlsval3  42514  disjinfi  45099  fourierdlem54  46081  fourierdlem76  46103  uhgrimisgrgriclem  47782