Theorem mpbi2and 935

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	|- ( ph -> ps )
mpbi2and.2	|- ( ph -> ch )
mpbi2and.3	|- ( ph -> ( ( ps /\ ch ) <-> th ) )

Assertion

Ref	Expression
mpbi2and	|- ( ph -> th )

Proof of Theorem mpbi2and

Step	Hyp	Ref	Expression
1		mpbi2and.1	. . 3 |- ( ph -> ps )
2		mpbi2and.2	. . 3 |- ( ph -> ch )
3	1, 2	jca 541	. 2 |- ( ph -> ( ps /\ ch ) )
4		mpbi2and.3	. 2 |- ( ph -> ( ( ps /\ ch ) <-> th ) )
5	3, 4	mpbid 215	1 |- ( ph -> th )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 376

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 190  df-an 378

This theorem is referenced by:  supiso  8009  hartogslem1  8075  cantnfp1lem3  8203  oemapwe  8217  cantnffval2  8218  mulne0d  10286  flflp1  12076  flval2  12082  remim  13257  ntrivcvgtail  14033  divalgmod  14466  divnumden  14776  numdensq  14782  prmdivdiv  14814  4sqlem7  14967  isposd  16279  latasymd  16381  latjidm  16398  latmidm  16410  latledi  16413  latjass  16419  mod1ile  16429  isglbd  16441  lubun  16447  poslubmo  16470  posglbmo  16471  ismgmid2  16588  oppginv  17088  slwhash  17354  lsmmod  17403  iscmnd  17520  dprd2da  17753  dmdprdsplit2lem  17756  dprdsplit  17759  pgpfac1lem1  17785  imasring  17925  isdrngd  18078  subrg1  18096  lsmsp  18387  lspprabs  18396  lsmcv  18442  psr1  18713  mat1  19549  topgele  20026  lmcn2  20741  dvdsq1p  23190  wilthlem2  24073  dchr1  24264  ismir  24783  atcvatlem  28119  ressprs  28491  rngurd  28625  ordtconlem1  28804  cvmliftphtlem  30112  cvmlift3lem6  30119  cvmlift3lem9  30122  poimirlem13  32017  poimirlem14  32018  lsatexch  32680  lsatcvatlem  32686  oldmm1  32854  olj01  32862  olm01  32873  cvrcmp  32920  atcvreq0  32951  cvlexchb1  32967  cvlcvr1  32976  exatleN  33040  hlrelat3  33048  cvrval3  33049  cvratlem  33057  atlelt  33074  cvrat3  33078  2atjm  33081  atbtwn  33082  hlatexch3N  33116  hlatexch4  33117  2llnmat  33160  2atm  33163  lplnexllnN  33200  2llnjaN  33202  4atlem11b  33244  4atlem12b  33247  2lplnja  33255  dalem1  33295  dalemcea  33296  dalem3  33300  dalem8  33306  dalem16  33315  dalem17  33316  dalem21  33330  dalem25  33334  dalem39  33347  dalem54  33362  dalem55  33363  dalem57  33365  dalem60  33368  2lnat  33420  2atm2atN  33421  2llnma1b  33422  cdlema1N  33427  paddasslem12  33467  paddasslem13  33468  pmodlem1  33482  dalawlem2  33508  dalawlem3  33509  dalawlem5  33511  dalawlem6  33512  dalawlem8  33514  dalawlem11  33517  dalawlem12  33518  osumcllem1N  33592  lhp2lt  33637  lhpexle2lem  33645  lhpexle3lem  33647  lhpocnle  33652  lhpat3  33682  4atexlemtlw  33703  4atexlemnclw  33706  4atexlemcnd  33708  lautj  33729  lautm  33730  trlval3  33824  cdlemc5  33832  cdlemd3  33837  cdleme3g  33871  cdleme3h  33872  cdleme7d  33883  cdleme11c  33898  cdleme11k  33905  cdleme15d  33914  cdleme16e  33919  cdleme16f  33920  cdleme17b  33924  cdlemednpq  33936  cdleme19a  33941  cdleme20j  33956  cdleme21c  33965  cdleme22aa  33977  cdleme22b  33979  cdleme22cN  33980  cdleme22d  33981  cdleme23c  33989  cdleme28a  34008  cdleme35a  34086  cdleme35b  34088  cdleme35f  34092  cdleme42i  34121  cdlemeg46req  34167  cdlemf2  34200  cdlemg4c  34250  cdlemg6c  34258  cdlemg8b  34266  cdlemg10  34279  cdlemg11b  34280  cdlemg12f  34286  cdlemg13a  34289  cdlemg17a  34299  cdlemg17dALTN  34302  cdlemg18b  34317  cdlemg19a  34321  cdlemg27a  34330  cdlemg33b0  34339  cdlemg35  34351  cdlemg42  34367  cdlemg46  34373  trljco  34378  tendopltp  34418  cdlemi  34458  cdlemk3  34471  cdlemk10  34481  cdlemk15  34493  cdlemk1u  34497  cdlemk39  34554  cdlemk50  34590  erng1lem  34625  erngdvlem4  34629  erngdvlem4-rN  34637  dialss  34685  dia2dimlem1  34703  dia2dimlem10  34712  dia2dimlem12  34714  cdlemm10N  34757  djajN  34776  diblss  34809  cdlemn2  34834  dihjustlem  34855  dihord1  34857  dihord2pre2  34865  dib2dim  34882  dih2dimb  34883  dih2dimbALTN  34884  dihopelvalcpre  34887  dihord5b  34898  dihord5apre  34901  dihmeetlem1N  34929  dihglblem5apreN  34930  dihglblem2N  34933  dihmeetlem2N  34938  dihmeetlem3N  34944  lclkrlem2f  35151  lclkrlem2v  35167  lclkrslem2  35177  lcfrlem25  35206  lcfrlem35  35216  mapdlsm  35303  fourierdlem54  38136  fourierdlem76  38158