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

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

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 395

This theorem is referenced by:  supiso  9472  hartogslem1  9539  cantnfp1lem3  9677  oemapwe  9691  cantnffval2  9692  mulne0d  11870  flflp1  13776  flval2  13783  remim  15068  ntrivcvgtail  15850  divalgmod  16353  divnumden  16688  numdensq  16694  prmdivdiv  16724  4sqlem7  16881  isposd  18280  poslubmo  18368  posglbmo  18369  latasymd  18402  latjidm  18419  latmidm  18431  latledi  18434  latjass  18440  mod1ile  18450  isglbd  18466  lubun  18472  ismgmid2  18593  oppginv  19267  slwhash  19533  lsmmod  19584  iscmnd  19703  dprd2da  19953  dmdprdsplit2lem  19956  dprdsplit  19959  pgpfac1lem1  19985  ringurd  20079  imasring  20218  subrg1  20472  isdrngd  20533  isdrngdOLD  20535  lsmsp  20841  lspprabs  20850  lsmcv  20899  psr1  21751  mat1  22169  lmcn2  23373  dvdsq1p  25913  wilthlem2  26809  dchr1  26996  ismir  28177  vdgfrgrgt2  29818  atcvatlem  31905  ressprs  32400  zarclssn  33151  ordtconnlem1  33202  cvmliftphtlem  34606  cvmlift3lem6  34613  cvmlift3lem9  34616  poimirlem13  36804  poimirlem14  36805  lsatexch  38216  lsatcvatlem  38222  oldmm1  38390  olj01  38398  olm01  38409  cvrcmp  38456  atcvreq0  38487  cvlexchb1  38503  cvlcvr1  38512  exatleN  38578  hlrelat3  38586  cvrval3  38587  cvratlem  38595  atlelt  38612  cvrat3  38616  2atjm  38619  atbtwn  38620  hlatexch3N  38654  hlatexch4  38655  2llnmat  38698  2atm  38701  lplnexllnN  38738  2llnjaN  38740  4atlem11b  38782  4atlem12b  38785  2lplnja  38793  dalem1  38833  dalemcea  38834  dalem3  38838  dalem8  38844  dalem16  38853  dalem17  38854  dalem21  38868  dalem25  38872  dalem39  38885  dalem54  38900  dalem55  38901  dalem57  38903  dalem60  38906  2lnat  38958  2atm2atN  38959  2llnma1b  38960  cdlema1N  38965  paddasslem12  39005  paddasslem13  39006  pmodlem1  39020  dalawlem2  39046  dalawlem3  39047  dalawlem5  39049  dalawlem6  39050  dalawlem8  39052  dalawlem11  39055  dalawlem12  39056  osumcllem1N  39130  lhp2lt  39175  lhpexle2lem  39183  lhpexle3lem  39185  lhpocnle  39190  lhpat3  39220  4atexlemtlw  39241  4atexlemnclw  39244  4atexlemcnd  39246  lautj  39267  lautm  39268  trlval3  39361  cdlemc5  39369  cdlemd3  39374  cdleme3g  39408  cdleme3h  39409  cdleme7d  39420  cdleme11c  39435  cdleme11k  39442  cdleme15d  39451  cdleme16e  39456  cdleme16f  39457  cdleme17b  39461  cdlemednpq  39473  cdleme19a  39477  cdleme20j  39492  cdleme21c  39501  cdleme22aa  39513  cdleme22b  39515  cdleme22cN  39516  cdleme22d  39517  cdleme23c  39525  cdleme28a  39544  cdleme35a  39622  cdleme35b  39624  cdleme35f  39628  cdleme42i  39657  cdlemeg46req  39703  cdlemf2  39736  cdlemg4c  39786  cdlemg6c  39794  cdlemg8b  39802  cdlemg10  39815  cdlemg11b  39816  cdlemg12f  39822  cdlemg13a  39825  cdlemg17a  39835  cdlemg17dALTN  39838  cdlemg18b  39853  cdlemg19a  39857  cdlemg27a  39866  cdlemg33b0  39875  cdlemg35  39887  cdlemg42  39903  cdlemg46  39909  trljco  39914  tendopltp  39954  cdlemi  39994  cdlemk3  40007  cdlemk10  40017  cdlemk15  40029  cdlemk1u  40033  cdlemk39  40090  cdlemk50  40126  erng1lem  40161  erngdvlem4  40165  erngdvlem4-rN  40173  dialss  40220  dia2dimlem1  40238  dia2dimlem10  40247  dia2dimlem12  40249  cdlemm10N  40292  djajN  40311  diblss  40344  cdlemn2  40369  dihjustlem  40390  dihord1  40392  dihord2pre2  40400  dib2dim  40417  dih2dimb  40418  dih2dimbALTN  40419  dihopelvalcpre  40422  dihord5b  40433  dihord5apre  40436  dihmeetlem1N  40464  dihglblem5apreN  40465  dihglblem2N  40468  dihmeetlem2N  40473  dihmeetlem3N  40479  lclkrlem2f  40686  lclkrlem2v  40702  lclkrslem2  40712  lcfrlem25  40741  lcfrlem35  40751  mapdlsm  40838  evlsval3  41433  numdenexp  41530  disjinfi  44189  fourierdlem54  45174  fourierdlem76  45196