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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  supiso  8923  hartogslem1  8990  cantnfp1lem3  9127  oemapwe  9141  cantnffval2  9142  mulne0d  11281  flflp1  13172  flval2  13179  remim  14468  ntrivcvgtail  15248  divalgmod  15747  divnumden  16078  numdensq  16084  prmdivdiv  16114  4sqlem7  16270  isposd  17557  latasymd  17659  latjidm  17676  latmidm  17688  latledi  17691  latjass  17697  mod1ile  17707  isglbd  17719  lubun  17725  poslubmo  17748  posglbmo  17749  ismgmid2  17870  oppginv  18479  slwhash  18741  lsmmod  18793  iscmnd  18911  dprd2da  19157  dmdprdsplit2lem  19160  dprdsplit  19163  pgpfac1lem1  19189  imasring  19365  isdrngd  19520  subrg1  19538  lsmsp  19851  lspprabs  19860  lsmcv  19906  psr1  20650  mat1  21052  lmcn2  22254  dvdsq1p  24761  wilthlem2  25654  dchr1  25841  ismir  26453  vdgfrgrgt2  28083  atcvatlem  30168  ressprs  30668  rngurd  30907  zarclssn  31226  ordtconnlem1  31277  cvmliftphtlem  32677  cvmlift3lem6  32684  cvmlift3lem9  32687  poimirlem13  35070  poimirlem14  35071  lsatexch  36339  lsatcvatlem  36345  oldmm1  36513  olj01  36521  olm01  36532  cvrcmp  36579  atcvreq0  36610  cvlexchb1  36626  cvlcvr1  36635  exatleN  36700  hlrelat3  36708  cvrval3  36709  cvratlem  36717  atlelt  36734  cvrat3  36738  2atjm  36741  atbtwn  36742  hlatexch3N  36776  hlatexch4  36777  2llnmat  36820  2atm  36823  lplnexllnN  36860  2llnjaN  36862  4atlem11b  36904  4atlem12b  36907  2lplnja  36915  dalem1  36955  dalemcea  36956  dalem3  36960  dalem8  36966  dalem16  36975  dalem17  36976  dalem21  36990  dalem25  36994  dalem39  37007  dalem54  37022  dalem55  37023  dalem57  37025  dalem60  37028  2lnat  37080  2atm2atN  37081  2llnma1b  37082  cdlema1N  37087  paddasslem12  37127  paddasslem13  37128  pmodlem1  37142  dalawlem2  37168  dalawlem3  37169  dalawlem5  37171  dalawlem6  37172  dalawlem8  37174  dalawlem11  37177  dalawlem12  37178  osumcllem1N  37252  lhp2lt  37297  lhpexle2lem  37305  lhpexle3lem  37307  lhpocnle  37312  lhpat3  37342  4atexlemtlw  37363  4atexlemnclw  37366  4atexlemcnd  37368  lautj  37389  lautm  37390  trlval3  37483  cdlemc5  37491  cdlemd3  37496  cdleme3g  37530  cdleme3h  37531  cdleme7d  37542  cdleme11c  37557  cdleme11k  37564  cdleme15d  37573  cdleme16e  37578  cdleme16f  37579  cdleme17b  37583  cdlemednpq  37595  cdleme19a  37599  cdleme20j  37614  cdleme21c  37623  cdleme22aa  37635  cdleme22b  37637  cdleme22cN  37638  cdleme22d  37639  cdleme23c  37647  cdleme28a  37666  cdleme35a  37744  cdleme35b  37746  cdleme35f  37750  cdleme42i  37779  cdlemeg46req  37825  cdlemf2  37858  cdlemg4c  37908  cdlemg6c  37916  cdlemg8b  37924  cdlemg10  37937  cdlemg11b  37938  cdlemg12f  37944  cdlemg13a  37947  cdlemg17a  37957  cdlemg17dALTN  37960  cdlemg18b  37975  cdlemg19a  37979  cdlemg27a  37988  cdlemg33b0  37997  cdlemg35  38009  cdlemg42  38025  cdlemg46  38031  trljco  38036  tendopltp  38076  cdlemi  38116  cdlemk3  38129  cdlemk10  38139  cdlemk15  38151  cdlemk1u  38155  cdlemk39  38212  cdlemk50  38248  erng1lem  38283  erngdvlem4  38287  erngdvlem4-rN  38295  dialss  38342  dia2dimlem1  38360  dia2dimlem10  38369  dia2dimlem12  38371  cdlemm10N  38414  djajN  38433  diblss  38466  cdlemn2  38491  dihjustlem  38512  dihord1  38514  dihord2pre2  38522  dib2dim  38539  dih2dimb  38540  dih2dimbALTN  38541  dihopelvalcpre  38544  dihord5b  38555  dihord5apre  38558  dihmeetlem1N  38586  dihglblem5apreN  38587  dihglblem2N  38590  dihmeetlem2N  38595  dihmeetlem3N  38601  lclkrlem2f  38808  lclkrlem2v  38824  lclkrslem2  38834  lcfrlem25  38863  lcfrlem35  38873  mapdlsm  38960  numdenexp  39494  disjinfi  41820  fourierdlem54  42802  fourierdlem76  42824