Theorem mpbi2and 710

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  supiso  8931  hartogslem1  8998  cantnfp1lem3  9135  oemapwe  9149  cantnffval2  9150  mulne0d  11284  flflp1  13169  flval2  13176  remim  14468  ntrivcvgtail  15248  divalgmod  15749  divnumden  16080  numdensq  16086  prmdivdiv  16116  4sqlem7  16272  isposd  17557  latasymd  17659  latjidm  17676  latmidm  17688  latledi  17691  latjass  17697  mod1ile  17707  isglbd  17719  lubun  17725  poslubmo  17748  posglbmo  17749  ismgmid2  17870  oppginv  18479  slwhash  18741  lsmmod  18793  iscmnd  18911  dprd2da  19156  dmdprdsplit2lem  19159  dprdsplit  19162  pgpfac1lem1  19188  imasring  19361  isdrngd  19519  subrg1  19537  lsmsp  19850  lspprabs  19859  lsmcv  19905  psr1  20184  mat1  21048  lmcn2  22249  dvdsq1p  24746  wilthlem2  25638  dchr1  25825  ismir  26437  vdgfrgrgt2  28069  atcvatlem  30154  ressprs  30635  rngurd  30850  ordtconnlem1  31160  cvmliftphtlem  32557  cvmlift3lem6  32564  cvmlift3lem9  32567  poimirlem13  34897  poimirlem14  34898  lsatexch  36171  lsatcvatlem  36177  oldmm1  36345  olj01  36353  olm01  36364  cvrcmp  36411  atcvreq0  36442  cvlexchb1  36458  cvlcvr1  36467  exatleN  36532  hlrelat3  36540  cvrval3  36541  cvratlem  36549  atlelt  36566  cvrat3  36570  2atjm  36573  atbtwn  36574  hlatexch3N  36608  hlatexch4  36609  2llnmat  36652  2atm  36655  lplnexllnN  36692  2llnjaN  36694  4atlem11b  36736  4atlem12b  36739  2lplnja  36747  dalem1  36787  dalemcea  36788  dalem3  36792  dalem8  36798  dalem16  36807  dalem17  36808  dalem21  36822  dalem25  36826  dalem39  36839  dalem54  36854  dalem55  36855  dalem57  36857  dalem60  36860  2lnat  36912  2atm2atN  36913  2llnma1b  36914  cdlema1N  36919  paddasslem12  36959  paddasslem13  36960  pmodlem1  36974  dalawlem2  37000  dalawlem3  37001  dalawlem5  37003  dalawlem6  37004  dalawlem8  37006  dalawlem11  37009  dalawlem12  37010  osumcllem1N  37084  lhp2lt  37129  lhpexle2lem  37137  lhpexle3lem  37139  lhpocnle  37144  lhpat3  37174  4atexlemtlw  37195  4atexlemnclw  37198  4atexlemcnd  37200  lautj  37221  lautm  37222  trlval3  37315  cdlemc5  37323  cdlemd3  37328  cdleme3g  37362  cdleme3h  37363  cdleme7d  37374  cdleme11c  37389  cdleme11k  37396  cdleme15d  37405  cdleme16e  37410  cdleme16f  37411  cdleme17b  37415  cdlemednpq  37427  cdleme19a  37431  cdleme20j  37446  cdleme21c  37455  cdleme22aa  37467  cdleme22b  37469  cdleme22cN  37470  cdleme22d  37471  cdleme23c  37479  cdleme28a  37498  cdleme35a  37576  cdleme35b  37578  cdleme35f  37582  cdleme42i  37611  cdlemeg46req  37657  cdlemf2  37690  cdlemg4c  37740  cdlemg6c  37748  cdlemg8b  37756  cdlemg10  37769  cdlemg11b  37770  cdlemg12f  37776  cdlemg13a  37779  cdlemg17a  37789  cdlemg17dALTN  37792  cdlemg18b  37807  cdlemg19a  37811  cdlemg27a  37820  cdlemg33b0  37829  cdlemg35  37841  cdlemg42  37857  cdlemg46  37863  trljco  37868  tendopltp  37908  cdlemi  37948  cdlemk3  37961  cdlemk10  37971  cdlemk15  37983  cdlemk1u  37987  cdlemk39  38044  cdlemk50  38080  erng1lem  38115  erngdvlem4  38119  erngdvlem4-rN  38127  dialss  38174  dia2dimlem1  38192  dia2dimlem10  38201  dia2dimlem12  38203  cdlemm10N  38246  djajN  38265  diblss  38298  cdlemn2  38323  dihjustlem  38344  dihord1  38346  dihord2pre2  38354  dib2dim  38371  dih2dimb  38372  dih2dimbALTN  38373  dihopelvalcpre  38376  dihord5b  38387  dihord5apre  38390  dihmeetlem1N  38418  dihglblem5apreN  38419  dihglblem2N  38422  dihmeetlem2N  38427  dihmeetlem3N  38433  lclkrlem2f  38640  lclkrlem2v  38656  lclkrslem2  38666  lcfrlem25  38695  lcfrlem35  38705  mapdlsm  38792  numdenexp  39176  fourierdlem54  42435  fourierdlem76  42457