Theorem mpbi2and 712

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 232	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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 207  df-an 396

This theorem is referenced by:  supiso  9370  hartogslem1  9438  cantnfp1lem3  9580  oemapwe  9594  cantnffval2  9595  mulne0d  11779  flflp1  13721  flval2  13728  remim  15034  ntrivcvgtail  15817  divalgmod  16327  divnumden  16669  numdensq  16675  numdenexp  16681  prmdivdiv  16708  4sqlem7  16866  isposd  18238  poslubmo  18325  posglbmo  18326  latasymd  18361  latjidm  18378  latmidm  18390  latledi  18393  latjass  18399  mod1ile  18409  isglbd  18425  lubun  18431  ismgmid2  18586  oppginv  19281  slwhash  19546  lsmmod  19597  iscmnd  19716  dprd2da  19966  dmdprdsplit2lem  19969  dprdsplit  19972  pgpfac1lem1  19998  ringurd  20113  imasring  20258  subrg1  20507  isdrngd  20690  isdrngdOLD  20692  lsmsp  21030  lspprabs  21039  lsmcv  21088  psr1  21918  mat1  22372  lmcn2  23574  dvdsq1p  26105  wilthlem2  27016  dchr1  27205  ismir  28647  vdgfrgrgt2  30289  atcvatlem  32376  ressprs  32958  rprmasso  33501  rprmasso3  33503  zarclssn  33897  ordtconnlem1  33948  cvmliftphtlem  35372  cvmlift3lem6  35379  cvmlift3lem9  35382  poimirlem13  37683  poimirlem14  37684  lsatexch  39152  lsatcvatlem  39158  oldmm1  39326  olj01  39334  olm01  39345  cvrcmp  39392  atcvreq0  39423  cvlexchb1  39439  cvlcvr1  39448  exatleN  39513  hlrelat3  39521  cvrval3  39522  cvratlem  39530  atlelt  39547  cvrat3  39551  2atjm  39554  atbtwn  39555  hlatexch3N  39589  hlatexch4  39590  2llnmat  39633  2atm  39636  lplnexllnN  39673  2llnjaN  39675  4atlem11b  39717  4atlem12b  39720  2lplnja  39728  dalem1  39768  dalemcea  39769  dalem3  39773  dalem8  39779  dalem16  39788  dalem17  39789  dalem21  39803  dalem25  39807  dalem39  39820  dalem54  39835  dalem55  39836  dalem57  39838  dalem60  39841  2lnat  39893  2atm2atN  39894  2llnma1b  39895  cdlema1N  39900  paddasslem12  39940  paddasslem13  39941  pmodlem1  39955  dalawlem2  39981  dalawlem3  39982  dalawlem5  39984  dalawlem6  39985  dalawlem8  39987  dalawlem11  39990  dalawlem12  39991  osumcllem1N  40065  lhp2lt  40110  lhpexle2lem  40118  lhpexle3lem  40120  lhpocnle  40125  lhpat3  40155  4atexlemtlw  40176  4atexlemnclw  40179  4atexlemcnd  40181  lautj  40202  lautm  40203  trlval3  40296  cdlemc5  40304  cdlemd3  40309  cdleme3g  40343  cdleme3h  40344  cdleme7d  40355  cdleme11c  40370  cdleme11k  40377  cdleme15d  40386  cdleme16e  40391  cdleme16f  40392  cdleme17b  40396  cdlemednpq  40408  cdleme19a  40412  cdleme20j  40427  cdleme21c  40436  cdleme22aa  40448  cdleme22b  40450  cdleme22cN  40451  cdleme22d  40452  cdleme23c  40460  cdleme28a  40479  cdleme35a  40557  cdleme35b  40559  cdleme35f  40563  cdleme42i  40592  cdlemeg46req  40638  cdlemf2  40671  cdlemg4c  40721  cdlemg6c  40729  cdlemg8b  40737  cdlemg10  40750  cdlemg11b  40751  cdlemg12f  40757  cdlemg13a  40760  cdlemg17a  40770  cdlemg17dALTN  40773  cdlemg18b  40788  cdlemg19a  40792  cdlemg27a  40801  cdlemg33b0  40810  cdlemg35  40822  cdlemg42  40838  cdlemg46  40844  trljco  40849  tendopltp  40889  cdlemi  40929  cdlemk3  40942  cdlemk10  40952  cdlemk15  40964  cdlemk1u  40968  cdlemk39  41025  cdlemk50  41061  erng1lem  41096  erngdvlem4  41100  erngdvlem4-rN  41108  dialss  41155  dia2dimlem1  41173  dia2dimlem10  41182  dia2dimlem12  41184  cdlemm10N  41227  djajN  41246  diblss  41279  cdlemn2  41304  dihjustlem  41325  dihord1  41327  dihord2pre2  41335  dib2dim  41352  dih2dimb  41353  dih2dimbALTN  41354  dihopelvalcpre  41357  dihord5b  41368  dihord5apre  41371  dihmeetlem1N  41399  dihglblem5apreN  41400  dihglblem2N  41403  dihmeetlem2N  41408  dihmeetlem3N  41414  lclkrlem2f  41621  lclkrlem2v  41637  lclkrslem2  41647  lcfrlem25  41676  lcfrlem35  41686  mapdlsm  41773  evlsval3  42667  disjinfi  45303  fourierdlem54  46272  fourierdlem76  46294  uhgrimisgrgriclem  48044