Theorem mpbi2and 888

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 519	. 2 |- ( ph -> ( ps /\ ch ) )
4		mpbi2and.3	. 2 |- ( ph -> ( ( ps /\ ch ) <-> th ) )
5	3, 4	mpbid 202	1 |- ( ph -> th )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359

This theorem is referenced by:  supiso  7433  hartogslem1  7467  cantnfp1lem3  7592  oemapwe  7606  cantnffval2  7607  mulne0d  9630  flval2  11176  remim  11877  divalgmod  12881  divnumden  13095  numdensq  13101  prmdivdiv  13131  4sqlem7  13267  isposd  14367  latasymd  14441  latjidm  14458  latmidm  14470  latledi  14473  latjass  14479  mod1ile  14489  isglbd  14499  lubun  14505  poslubmo  14528  ismgmid2  14668  oppginv  15110  slwhash  15213  lsmmod  15262  iscmnd  15379  dprd2da  15555  dmdprdsplit2lem  15558  dprdsplit  15561  pgpfac1lem1  15587  imasrng  15680  isdrngd  15815  subrg1  15833  lsmsp  16113  lspprabs  16122  lsmcv  16168  psr1  16430  topgele  16954  lmcn2  17634  dvdsq1p  20036  wilthlem2  20805  dchr1  20994  atcvatlem  23841  cvmliftphtlem  24957  cvmlift3lem6  24964  cvmlift3lem9  24967  ntrivcvgtail  25181  lxflflp1  26142  mat1  27350  swrdccat3b  28031  lubunNEW  29456  lsatexch  29526  lsatcvatlem  29532  oldmm1  29700  olj01  29708  olm01  29719  cvrcmp  29766  atcvreq0  29797  cvlexchb1  29813  cvlcvr1  29822  exatleN  29886  hlrelat3  29894  cvrval3  29895  cvratlem  29903  atlelt  29920  cvrat3  29924  2atjm  29927  atbtwn  29928  hlatexch3N  29962  hlatexch4  29963  2llnmat  30006  2atm  30009  lplnexllnN  30046  2llnjaN  30048  4atlem11b  30090  4atlem12b  30093  2lplnja  30101  dalem1  30141  dalemcea  30142  dalem3  30146  dalem8  30152  dalem16  30161  dalem17  30162  dalem21  30176  dalem25  30180  dalem39  30193  dalem54  30208  dalem55  30209  dalem57  30211  dalem60  30214  2lnat  30266  2atm2atN  30267  2llnma1b  30268  cdlema1N  30273  paddasslem12  30313  paddasslem13  30314  pmodlem1  30328  dalawlem2  30354  dalawlem3  30355  dalawlem5  30357  dalawlem6  30358  dalawlem8  30360  dalawlem11  30363  dalawlem12  30364  osumcllem1N  30438  lhp2lt  30483  lhpexle2lem  30491  lhpexle3lem  30493  lhpocnle  30498  lhpat3  30528  4atexlemtlw  30549  4atexlemnclw  30552  4atexlemcnd  30554  lautj  30575  lautm  30576  trlval3  30669  cdlemc5  30677  cdlemd3  30682  cdleme3g  30716  cdleme3h  30717  cdleme7d  30728  cdleme11c  30743  cdleme11k  30750  cdleme15d  30759  cdleme16e  30764  cdleme16f  30765  cdleme17b  30769  cdlemednpq  30781  cdleme19a  30785  cdleme20j  30800  cdleme21c  30809  cdleme22aa  30821  cdleme22b  30823  cdleme22cN  30824  cdleme22d  30825  cdleme23c  30833  cdleme28a  30852  cdleme35a  30930  cdleme35b  30932  cdleme35f  30936  cdleme42i  30965  cdlemeg46req  31011  cdlemf2  31044  cdlemg4c  31094  cdlemg6c  31102  cdlemg8b  31110  cdlemg10  31123  cdlemg11b  31124  cdlemg12f  31130  cdlemg13a  31133  cdlemg17a  31143  cdlemg17dALTN  31146  cdlemg18b  31161  cdlemg19a  31165  cdlemg27a  31174  cdlemg33b0  31183  cdlemg35  31195  cdlemg42  31211  cdlemg46  31217  trljco  31222  tendopltp  31262  cdlemi  31302  cdlemk3  31315  cdlemk10  31325  cdlemk15  31337  cdlemk1u  31341  cdlemk39  31398  cdlemk50  31434  erng1lem  31469  erngdvlem4  31473  erngdvlem4-rN  31481  dialss  31529  dia2dimlem1  31547  dia2dimlem10  31556  dia2dimlem12  31558  cdlemm10N  31601  djajN  31620  diblss  31653  cdlemn2  31678  dihjustlem  31699  dihord1  31701  dihord2pre2  31709  dib2dim  31726  dih2dimb  31727  dih2dimbALTN  31728  dihopelvalcpre  31731  dihord5b  31742  dihord5apre  31745  dihmeetlem1N  31773  dihglblem5apreN  31774  dihglblem2N  31777  dihmeetlem2N  31782  dihmeetlem3N  31788  lclkrlem2f  31995  lclkrlem2v  32011  lclkrslem2  32021  lcfrlem25  32050  lcfrlem35  32060  mapdlsm  32147

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361