Theorem mpbi2and 708

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  supiso  9164  hartogslem1  9231  cantnfp1lem3  9368  oemapwe  9382  cantnffval2  9383  mulne0d  11557  flflp1  13455  flval2  13462  remim  14756  ntrivcvgtail  15540  divalgmod  16043  divnumden  16380  numdensq  16386  prmdivdiv  16416  4sqlem7  16573  isposd  17956  poslubmo  18044  posglbmo  18045  latasymd  18078  latjidm  18095  latmidm  18107  latledi  18110  latjass  18116  mod1ile  18126  isglbd  18142  lubun  18148  ismgmid2  18267  oppginv  18881  slwhash  19144  lsmmod  19196  iscmnd  19314  dprd2da  19560  dmdprdsplit2lem  19563  dprdsplit  19566  pgpfac1lem1  19592  imasring  19773  isdrngd  19931  subrg1  19949  lsmsp  20263  lspprabs  20272  lsmcv  20318  psr1  21091  mat1  21504  lmcn2  22708  dvdsq1p  25230  wilthlem2  26123  dchr1  26310  ismir  26924  vdgfrgrgt2  28563  atcvatlem  30648  ressprs  31143  rngurd  31384  zarclssn  31725  ordtconnlem1  31776  cvmliftphtlem  33179  cvmlift3lem6  33186  cvmlift3lem9  33189  poimirlem13  35717  poimirlem14  35718  lsatexch  36984  lsatcvatlem  36990  oldmm1  37158  olj01  37166  olm01  37177  cvrcmp  37224  atcvreq0  37255  cvlexchb1  37271  cvlcvr1  37280  exatleN  37345  hlrelat3  37353  cvrval3  37354  cvratlem  37362  atlelt  37379  cvrat3  37383  2atjm  37386  atbtwn  37387  hlatexch3N  37421  hlatexch4  37422  2llnmat  37465  2atm  37468  lplnexllnN  37505  2llnjaN  37507  4atlem11b  37549  4atlem12b  37552  2lplnja  37560  dalem1  37600  dalemcea  37601  dalem3  37605  dalem8  37611  dalem16  37620  dalem17  37621  dalem21  37635  dalem25  37639  dalem39  37652  dalem54  37667  dalem55  37668  dalem57  37670  dalem60  37673  2lnat  37725  2atm2atN  37726  2llnma1b  37727  cdlema1N  37732  paddasslem12  37772  paddasslem13  37773  pmodlem1  37787  dalawlem2  37813  dalawlem3  37814  dalawlem5  37816  dalawlem6  37817  dalawlem8  37819  dalawlem11  37822  dalawlem12  37823  osumcllem1N  37897  lhp2lt  37942  lhpexle2lem  37950  lhpexle3lem  37952  lhpocnle  37957  lhpat3  37987  4atexlemtlw  38008  4atexlemnclw  38011  4atexlemcnd  38013  lautj  38034  lautm  38035  trlval3  38128  cdlemc5  38136  cdlemd3  38141  cdleme3g  38175  cdleme3h  38176  cdleme7d  38187  cdleme11c  38202  cdleme11k  38209  cdleme15d  38218  cdleme16e  38223  cdleme16f  38224  cdleme17b  38228  cdlemednpq  38240  cdleme19a  38244  cdleme20j  38259  cdleme21c  38268  cdleme22aa  38280  cdleme22b  38282  cdleme22cN  38283  cdleme22d  38284  cdleme23c  38292  cdleme28a  38311  cdleme35a  38389  cdleme35b  38391  cdleme35f  38395  cdleme42i  38424  cdlemeg46req  38470  cdlemf2  38503  cdlemg4c  38553  cdlemg6c  38561  cdlemg8b  38569  cdlemg10  38582  cdlemg11b  38583  cdlemg12f  38589  cdlemg13a  38592  cdlemg17a  38602  cdlemg17dALTN  38605  cdlemg18b  38620  cdlemg19a  38624  cdlemg27a  38633  cdlemg33b0  38642  cdlemg35  38654  cdlemg42  38670  cdlemg46  38676  trljco  38681  tendopltp  38721  cdlemi  38761  cdlemk3  38774  cdlemk10  38784  cdlemk15  38796  cdlemk1u  38800  cdlemk39  38857  cdlemk50  38893  erng1lem  38928  erngdvlem4  38932  erngdvlem4-rN  38940  dialss  38987  dia2dimlem1  39005  dia2dimlem10  39014  dia2dimlem12  39016  cdlemm10N  39059  djajN  39078  diblss  39111  cdlemn2  39136  dihjustlem  39157  dihord1  39159  dihord2pre2  39167  dib2dim  39184  dih2dimb  39185  dih2dimbALTN  39186  dihopelvalcpre  39189  dihord5b  39200  dihord5apre  39203  dihmeetlem1N  39231  dihglblem5apreN  39232  dihglblem2N  39235  dihmeetlem2N  39240  dihmeetlem3N  39246  lclkrlem2f  39453  lclkrlem2v  39469  lclkrslem2  39479  lcfrlem25  39508  lcfrlem35  39518  mapdlsm  39605  evlsval3  40195  numdenexp  40258  disjinfi  42620  fourierdlem54  43591  fourierdlem76  43613