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  9468  hartogslem1  9536  cantnfp1lem3  9681  oemapwe  9695  cantnffval2  9696  mulne0d  11968  flflp1  13947  flval2  13954  remim  15284  ntrivcvgtail  16069  divalgmod  16576  divnumden  16924  numdensq  16930  numdenexp  16937  prmdivdiv  16964  4sqlem7  17122  isposd  18496  poslubmo  18583  posglbmo  18584  latasymd  18619  latjidm  18636  latmidm  18648  latledi  18651  latjass  18657  mod1ile  18667  isglbd  18683  lubun  18689  ismgmid2  18849  idressid  18862  oppginv  19573  slwhash  19838  lsmmod  19889  iscmnd  20008  dprd2da  20258  dmdprdsplit2lem  20261  dprdsplit  20264  pgpfac1lem1  20290  ringurd  20411  imasring  20560  subrg1  20834  isdrngd  21022  isdrngdOLD  21024  lsmsp  21361  lspprabs  21370  lsmcv  21419  psr1  22278  evlsval3  22398  mat1  22762  lmcn2  23968  dvdsq1p  26481  wilthlem2  27396  dchr1  27584  ismir  29131  vdgfrgrgt2  30899  atcvatlem  32987  ressprs  33527  rprmasso  34057  rprmasso3  34059  zarclssn  34505  ordtconnlem1  34556  cvmliftphtlem  36082  cvmlift3lem6  36089  cvmlift3lem9  36092  poimirlem13  38552  poimirlem14  38553  lsatexch  40101  lsatcvatlem  40107  oldmm1  40275  olj01  40283  olm01  40294  cvrcmp  40341  atcvreq0  40372  cvlexchb1  40388  cvlcvr1  40397  exatleN  40462  hlrelat3  40470  cvrval3  40471  cvratlem  40479  atlelt  40496  cvrat3  40500  2atjm  40503  atbtwn  40504  hlatexch3N  40538  hlatexch4  40539  2llnmat  40582  2atm  40585  lplnexllnN  40622  2llnjaN  40624  4atlem11b  40666  4atlem12b  40669  2lplnja  40677  dalem1  40717  dalemcea  40718  dalem3  40722  dalem8  40728  dalem16  40737  dalem17  40738  dalem21  40752  dalem25  40756  dalem39  40769  dalem54  40784  dalem55  40785  dalem57  40787  dalem60  40790  2lnat  40842  2atm2atN  40843  2llnma1b  40844  cdlema1N  40849  paddasslem12  40889  paddasslem13  40890  pmodlem1  40904  dalawlem2  40930  dalawlem3  40931  dalawlem5  40933  dalawlem6  40934  dalawlem8  40936  dalawlem11  40939  dalawlem12  40940  osumcllem1N  41014  lhp2lt  41059  lhpexle2lem  41067  lhpexle3lem  41069  lhpocnle  41074  lhpat3  41104  4atexlemtlw  41125  4atexlemnclw  41128  4atexlemcnd  41130  lautj  41151  lautm  41152  trlval3  41245  cdlemc5  41253  cdlemd3  41258  cdleme3g  41292  cdleme3h  41293  cdleme7d  41304  cdleme11c  41319  cdleme11k  41326  cdleme15d  41335  cdleme16e  41340  cdleme16f  41341  cdleme17b  41345  cdlemednpq  41357  cdleme19a  41361  cdleme20j  41376  cdleme21c  41385  cdleme22aa  41397  cdleme22b  41399  cdleme22cN  41400  cdleme22d  41401  cdleme23c  41409  cdleme28a  41428  cdleme35a  41506  cdleme35b  41508  cdleme35f  41512  cdleme42i  41541  cdlemeg46req  41587  cdlemf2  41620  cdlemg4c  41670  cdlemg6c  41678  cdlemg8b  41686  cdlemg10  41699  cdlemg11b  41700  cdlemg12f  41706  cdlemg13a  41709  cdlemg17a  41719  cdlemg17dALTN  41722  cdlemg18b  41737  cdlemg19a  41741  cdlemg27a  41750  cdlemg33b0  41759  cdlemg35  41771  cdlemg42  41787  cdlemg46  41793  trljco  41798  tendopltp  41838  cdlemi  41878  cdlemk3  41891  cdlemk10  41901  cdlemk15  41913  cdlemk1u  41917  cdlemk39  41974  cdlemk50  42010  erng1lem  42045  erngdvlem4  42049  erngdvlem4-rN  42057  dialss  42104  dia2dimlem1  42122  dia2dimlem10  42131  dia2dimlem12  42133  cdlemm10N  42176  djajN  42195  diblss  42228  cdlemn2  42253  dihjustlem  42274  dihord1  42276  dihord2pre2  42284  dib2dim  42301  dih2dimb  42302  dih2dimbALTN  42303  dihopelvalcpre  42306  dihord5b  42317  dihord5apre  42320  dihmeetlem1N  42348  dihglblem5apreN  42349  dihglblem2N  42352  dihmeetlem2N  42357  dihmeetlem3N  42363  lclkrlem2f  42570  lclkrlem2v  42586  lclkrslem2  42596  lcfrlem25  42625  lcfrlem35  42635  mapdlsm  42722  disjinfi  46207  fourierdlem54  47170  fourierdlem76  47192  uhgrimisgrgriclem  49028