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  9452  hartogslem1  9520  cantnfp1lem3  9665  oemapwe  9679  cantnffval2  9680  mulne0d  11949  flflp1  13927  flval2  13934  remim  15264  ntrivcvgtail  16049  divalgmod  16556  divnumden  16904  numdensq  16910  numdenexp  16917  prmdivdiv  16944  4sqlem7  17102  isposd  18476  poslubmo  18563  posglbmo  18564  latasymd  18599  latjidm  18616  latmidm  18628  latledi  18631  latjass  18637  mod1ile  18647  isglbd  18663  lubun  18669  ismgmid2  18829  idressid  18842  oppginv  19553  slwhash  19818  lsmmod  19869  iscmnd  19988  dprd2da  20238  dmdprdsplit2lem  20241  dprdsplit  20244  pgpfac1lem1  20270  ringurd  20391  imasring  20540  subrg1  20814  isdrngd  21002  isdrngdOLD  21004  lsmsp  21341  lspprabs  21350  lsmcv  21399  psr1  22258  evlsval3  22378  mat1  22742  lmcn2  23948  dvdsq1p  26461  wilthlem2  27378  dchr1  27566  ismir  29113  vdgfrgrgt2  30881  atcvatlem  32969  ressprs  33509  rprmasso  34039  rprmasso3  34041  zarclssn  34487  ordtconnlem1  34538  cvmliftphtlem  36051  cvmlift3lem6  36058  cvmlift3lem9  36061  poimirlem13  38519  poimirlem14  38520  lsatexch  40068  lsatcvatlem  40074  oldmm1  40242  olj01  40250  olm01  40261  cvrcmp  40308  atcvreq0  40339  cvlexchb1  40355  cvlcvr1  40364  exatleN  40429  hlrelat3  40437  cvrval3  40438  cvratlem  40446  atlelt  40463  cvrat3  40467  2atjm  40470  atbtwn  40471  hlatexch3N  40505  hlatexch4  40506  2llnmat  40549  2atm  40552  lplnexllnN  40589  2llnjaN  40591  4atlem11b  40633  4atlem12b  40636  2lplnja  40644  dalem1  40684  dalemcea  40685  dalem3  40689  dalem8  40695  dalem16  40704  dalem17  40705  dalem21  40719  dalem25  40723  dalem39  40736  dalem54  40751  dalem55  40752  dalem57  40754  dalem60  40757  2lnat  40809  2atm2atN  40810  2llnma1b  40811  cdlema1N  40816  paddasslem12  40856  paddasslem13  40857  pmodlem1  40871  dalawlem2  40897  dalawlem3  40898  dalawlem5  40900  dalawlem6  40901  dalawlem8  40903  dalawlem11  40906  dalawlem12  40907  osumcllem1N  40981  lhp2lt  41026  lhpexle2lem  41034  lhpexle3lem  41036  lhpocnle  41041  lhpat3  41071  4atexlemtlw  41092  4atexlemnclw  41095  4atexlemcnd  41097  lautj  41118  lautm  41119  trlval3  41212  cdlemc5  41220  cdlemd3  41225  cdleme3g  41259  cdleme3h  41260  cdleme7d  41271  cdleme11c  41286  cdleme11k  41293  cdleme15d  41302  cdleme16e  41307  cdleme16f  41308  cdleme17b  41312  cdlemednpq  41324  cdleme19a  41328  cdleme20j  41343  cdleme21c  41352  cdleme22aa  41364  cdleme22b  41366  cdleme22cN  41367  cdleme22d  41368  cdleme23c  41376  cdleme28a  41395  cdleme35a  41473  cdleme35b  41475  cdleme35f  41479  cdleme42i  41508  cdlemeg46req  41554  cdlemf2  41587  cdlemg4c  41637  cdlemg6c  41645  cdlemg8b  41653  cdlemg10  41666  cdlemg11b  41667  cdlemg12f  41673  cdlemg13a  41676  cdlemg17a  41686  cdlemg17dALTN  41689  cdlemg18b  41704  cdlemg19a  41708  cdlemg27a  41717  cdlemg33b0  41726  cdlemg35  41738  cdlemg42  41754  cdlemg46  41760  trljco  41765  tendopltp  41805  cdlemi  41845  cdlemk3  41858  cdlemk10  41868  cdlemk15  41880  cdlemk1u  41884  cdlemk39  41941  cdlemk50  41977  erng1lem  42012  erngdvlem4  42016  erngdvlem4-rN  42024  dialss  42071  dia2dimlem1  42089  dia2dimlem10  42098  dia2dimlem12  42100  cdlemm10N  42143  djajN  42162  diblss  42195  cdlemn2  42220  dihjustlem  42241  dihord1  42243  dihord2pre2  42251  dib2dim  42268  dih2dimb  42269  dih2dimbALTN  42270  dihopelvalcpre  42273  dihord5b  42284  dihord5apre  42287  dihmeetlem1N  42315  dihglblem5apreN  42316  dihglblem2N  42319  dihmeetlem2N  42324  dihmeetlem3N  42330  lclkrlem2f  42537  lclkrlem2v  42553  lclkrslem2  42563  lcfrlem25  42592  lcfrlem35  42602  mapdlsm  42689  disjinfi  46150  fourierdlem54  47114  fourierdlem76  47136  uhgrimisgrgriclem  48972