Theorem mpbi2and 725

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  supiso  9446  hartogslem1  9514  cantnfp1lem3  9659  oemapwe  9673  cantnffval2  9674  mulne0d  11884  flflp1  13860  flval2  13867  remim  15194  ntrivcvgtail  15980  divalgmod  16489  divnumden  16832  numdensq  16838  numdenexp  16844  prmdivdiv  16871  4sqlem7  17029  isposd  18403  poslubmo  18490  posglbmo  18491  latasymd  18526  latjidm  18543  latmidm  18555  latledi  18558  latjass  18564  mod1ile  18574  isglbd  18590  lubun  18596  ismgmid2  18752  idressid  18762  oppginv  19460  slwhash  19725  lsmmod  19776  iscmnd  19895  dprd2da  20145  dmdprdsplit2lem  20148  dprdsplit  20151  pgpfac1lem1  20177  ringurd  20298  imasring  20445  subrg1  20718  isdrngd  20905  isdrngdOLD  20907  lsmsp  21244  lspprabs  21253  lsmcv  21302  psr1  22157  evlsval3  22277  mat1  22641  lmcn2  23843  dvdsq1p  26357  wilthlem2  27270  dchr1  27458  ismir  28973  vdgfrgrgt2  30686  atcvatlem  32774  ressprs  33317  rprmasso  33846  rprmasso3  33848  zarclssn  34294  ordtconnlem1  34345  cvmliftphtlem  35829  cvmlift3lem6  35836  cvmlift3lem9  35839  poimirlem13  38324  poimirlem14  38325  lsatexch  39857  lsatcvatlem  39863  oldmm1  40031  olj01  40039  olm01  40050  cvrcmp  40097  atcvreq0  40128  cvlexchb1  40144  cvlcvr1  40153  exatleN  40218  hlrelat3  40226  cvrval3  40227  cvratlem  40235  atlelt  40252  cvrat3  40256  2atjm  40259  atbtwn  40260  hlatexch3N  40294  hlatexch4  40295  2llnmat  40338  2atm  40341  lplnexllnN  40378  2llnjaN  40380  4atlem11b  40422  4atlem12b  40425  2lplnja  40433  dalem1  40473  dalemcea  40474  dalem3  40478  dalem8  40484  dalem16  40493  dalem17  40494  dalem21  40508  dalem25  40512  dalem39  40525  dalem54  40540  dalem55  40541  dalem57  40543  dalem60  40546  2lnat  40598  2atm2atN  40599  2llnma1b  40600  cdlema1N  40605  paddasslem12  40645  paddasslem13  40646  pmodlem1  40660  dalawlem2  40686  dalawlem3  40687  dalawlem5  40689  dalawlem6  40690  dalawlem8  40692  dalawlem11  40695  dalawlem12  40696  osumcllem1N  40770  lhp2lt  40815  lhpexle2lem  40823  lhpexle3lem  40825  lhpocnle  40830  lhpat3  40860  4atexlemtlw  40881  4atexlemnclw  40884  4atexlemcnd  40886  lautj  40907  lautm  40908  trlval3  41001  cdlemc5  41009  cdlemd3  41014  cdleme3g  41048  cdleme3h  41049  cdleme7d  41060  cdleme11c  41075  cdleme11k  41082  cdleme15d  41091  cdleme16e  41096  cdleme16f  41097  cdleme17b  41101  cdlemednpq  41113  cdleme19a  41117  cdleme20j  41132  cdleme21c  41141  cdleme22aa  41153  cdleme22b  41155  cdleme22cN  41156  cdleme22d  41157  cdleme23c  41165  cdleme28a  41184  cdleme35a  41262  cdleme35b  41264  cdleme35f  41268  cdleme42i  41297  cdlemeg46req  41343  cdlemf2  41376  cdlemg4c  41426  cdlemg6c  41434  cdlemg8b  41442  cdlemg10  41455  cdlemg11b  41456  cdlemg12f  41462  cdlemg13a  41465  cdlemg17a  41475  cdlemg17dALTN  41478  cdlemg18b  41493  cdlemg19a  41497  cdlemg27a  41506  cdlemg33b0  41515  cdlemg35  41527  cdlemg42  41543  cdlemg46  41549  trljco  41554  tendopltp  41594  cdlemi  41634  cdlemk3  41647  cdlemk10  41657  cdlemk15  41669  cdlemk1u  41673  cdlemk39  41730  cdlemk50  41766  erng1lem  41801  erngdvlem4  41805  erngdvlem4-rN  41813  dialss  41860  dia2dimlem1  41878  dia2dimlem10  41887  dia2dimlem12  41889  cdlemm10N  41932  djajN  41951  diblss  41984  cdlemn2  42009  dihjustlem  42030  dihord1  42032  dihord2pre2  42040  dib2dim  42057  dih2dimb  42058  dih2dimbALTN  42059  dihopelvalcpre  42062  dihord5b  42073  dihord5apre  42076  dihmeetlem1N  42104  dihglblem5apreN  42105  dihglblem2N  42108  dihmeetlem2N  42113  dihmeetlem3N  42119  lclkrlem2f  42326  lclkrlem2v  42342  lclkrslem2  42352  lcfrlem25  42381  lcfrlem35  42391  mapdlsm  42478  disjinfi  45950  fourierdlem54  46914  fourierdlem76  46936  uhgrimisgrgriclem  48735