Theorem mpbi2and 718

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  supiso  9386  hartogslem1  9454  cantnfp1lem3  9599  oemapwe  9613  cantnffval2  9614  mulne0d  11800  flflp1  13764  flval2  13771  remim  15077  ntrivcvgtail  15863  divalgmod  16373  divnumden  16716  numdensq  16722  numdenexp  16728  prmdivdiv  16755  4sqlem7  16913  isposd  18286  poslubmo  18373  posglbmo  18374  latasymd  18409  latjidm  18426  latmidm  18438  latledi  18441  latjass  18447  mod1ile  18457  isglbd  18473  lubun  18479  ismgmid2  18634  oppginv  19332  slwhash  19597  lsmmod  19648  iscmnd  19767  dprd2da  20017  dmdprdsplit2lem  20020  dprdsplit  20023  pgpfac1lem1  20049  ringurd  20164  imasring  20308  subrg1  20561  isdrngd  20744  isdrngdOLD  20746  lsmsp  21083  lspprabs  21092  lsmcv  21141  psr1  21952  evlsval3  22072  mat1  22437  lmcn2  23639  dvdsq1p  26153  wilthlem2  27057  dchr1  27245  ismir  28752  vdgfrgrgt2  30393  atcvatlem  32481  ressprs  33052  rprmasso  33615  rprmasso3  33617  zarclssn  34064  ordtconnlem1  34115  cvmliftphtlem  35552  cvmlift3lem6  35559  cvmlift3lem9  35562  poimirlem13  38007  poimirlem14  38008  lsatexch  39542  lsatcvatlem  39548  oldmm1  39716  olj01  39724  olm01  39735  cvrcmp  39782  atcvreq0  39813  cvlexchb1  39829  cvlcvr1  39838  exatleN  39903  hlrelat3  39911  cvrval3  39912  cvratlem  39920  atlelt  39937  cvrat3  39941  2atjm  39944  atbtwn  39945  hlatexch3N  39979  hlatexch4  39980  2llnmat  40023  2atm  40026  lplnexllnN  40063  2llnjaN  40065  4atlem11b  40107  4atlem12b  40110  2lplnja  40118  dalem1  40158  dalemcea  40159  dalem3  40163  dalem8  40169  dalem16  40178  dalem17  40179  dalem21  40193  dalem25  40197  dalem39  40210  dalem54  40225  dalem55  40226  dalem57  40228  dalem60  40231  2lnat  40283  2atm2atN  40284  2llnma1b  40285  cdlema1N  40290  paddasslem12  40330  paddasslem13  40331  pmodlem1  40345  dalawlem2  40371  dalawlem3  40372  dalawlem5  40374  dalawlem6  40375  dalawlem8  40377  dalawlem11  40380  dalawlem12  40381  osumcllem1N  40455  lhp2lt  40500  lhpexle2lem  40508  lhpexle3lem  40510  lhpocnle  40515  lhpat3  40545  4atexlemtlw  40566  4atexlemnclw  40569  4atexlemcnd  40571  lautj  40592  lautm  40593  trlval3  40686  cdlemc5  40694  cdlemd3  40699  cdleme3g  40733  cdleme3h  40734  cdleme7d  40745  cdleme11c  40760  cdleme11k  40767  cdleme15d  40776  cdleme16e  40781  cdleme16f  40782  cdleme17b  40786  cdlemednpq  40798  cdleme19a  40802  cdleme20j  40817  cdleme21c  40826  cdleme22aa  40838  cdleme22b  40840  cdleme22cN  40841  cdleme22d  40842  cdleme23c  40850  cdleme28a  40869  cdleme35a  40947  cdleme35b  40949  cdleme35f  40953  cdleme42i  40982  cdlemeg46req  41028  cdlemf2  41061  cdlemg4c  41111  cdlemg6c  41119  cdlemg8b  41127  cdlemg10  41140  cdlemg11b  41141  cdlemg12f  41147  cdlemg13a  41150  cdlemg17a  41160  cdlemg17dALTN  41163  cdlemg18b  41178  cdlemg19a  41182  cdlemg27a  41191  cdlemg33b0  41200  cdlemg35  41212  cdlemg42  41228  cdlemg46  41234  trljco  41239  tendopltp  41279  cdlemi  41319  cdlemk3  41332  cdlemk10  41342  cdlemk15  41354  cdlemk1u  41358  cdlemk39  41415  cdlemk50  41451  erng1lem  41486  erngdvlem4  41490  erngdvlem4-rN  41498  dialss  41545  dia2dimlem1  41563  dia2dimlem10  41572  dia2dimlem12  41574  cdlemm10N  41617  djajN  41636  diblss  41669  cdlemn2  41694  dihjustlem  41715  dihord1  41717  dihord2pre2  41725  dib2dim  41742  dih2dimb  41743  dih2dimbALTN  41744  dihopelvalcpre  41747  dihord5b  41758  dihord5apre  41761  dihmeetlem1N  41789  dihglblem5apreN  41790  dihglblem2N  41793  dihmeetlem2N  41798  dihmeetlem3N  41804  lclkrlem2f  42011  lclkrlem2v  42027  lclkrslem2  42037  lcfrlem25  42066  lcfrlem35  42076  mapdlsm  42163  disjinfi  45646  fourierdlem54  46610  fourierdlem76  46632  uhgrimisgrgriclem  48428