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  9385  hartogslem1  9453  cantnfp1lem3  9595  oemapwe  9609  cantnffval2  9610  mulne0d  11790  flflp1  13729  flval2  13736  remim  15042  ntrivcvgtail  15825  divalgmod  16335  divnumden  16677  numdensq  16683  numdenexp  16689  prmdivdiv  16716  4sqlem7  16874  isposd  18246  poslubmo  18333  posglbmo  18334  latasymd  18369  latjidm  18386  latmidm  18398  latledi  18401  latjass  18407  mod1ile  18417  isglbd  18433  lubun  18439  ismgmid2  18560  oppginv  19256  slwhash  19521  lsmmod  19572  iscmnd  19691  dprd2da  19941  dmdprdsplit2lem  19944  dprdsplit  19947  pgpfac1lem1  19973  ringurd  20088  imasring  20233  subrg1  20485  isdrngd  20668  isdrngdOLD  20670  lsmsp  21008  lspprabs  21017  lsmcv  21066  psr1  21896  mat1  22350  lmcn2  23552  dvdsq1p  26084  wilthlem2  26995  dchr1  27184  ismir  28622  vdgfrgrgt2  30260  atcvatlem  32347  ressprs  32921  rprmasso  33472  rprmasso3  33474  zarclssn  33839  ordtconnlem1  33890  cvmliftphtlem  35289  cvmlift3lem6  35296  cvmlift3lem9  35299  poimirlem13  37612  poimirlem14  37613  lsatexch  39021  lsatcvatlem  39027  oldmm1  39195  olj01  39203  olm01  39214  cvrcmp  39261  atcvreq0  39292  cvlexchb1  39308  cvlcvr1  39317  exatleN  39383  hlrelat3  39391  cvrval3  39392  cvratlem  39400  atlelt  39417  cvrat3  39421  2atjm  39424  atbtwn  39425  hlatexch3N  39459  hlatexch4  39460  2llnmat  39503  2atm  39506  lplnexllnN  39543  2llnjaN  39545  4atlem11b  39587  4atlem12b  39590  2lplnja  39598  dalem1  39638  dalemcea  39639  dalem3  39643  dalem8  39649  dalem16  39658  dalem17  39659  dalem21  39673  dalem25  39677  dalem39  39690  dalem54  39705  dalem55  39706  dalem57  39708  dalem60  39711  2lnat  39763  2atm2atN  39764  2llnma1b  39765  cdlema1N  39770  paddasslem12  39810  paddasslem13  39811  pmodlem1  39825  dalawlem2  39851  dalawlem3  39852  dalawlem5  39854  dalawlem6  39855  dalawlem8  39857  dalawlem11  39860  dalawlem12  39861  osumcllem1N  39935  lhp2lt  39980  lhpexle2lem  39988  lhpexle3lem  39990  lhpocnle  39995  lhpat3  40025  4atexlemtlw  40046  4atexlemnclw  40049  4atexlemcnd  40051  lautj  40072  lautm  40073  trlval3  40166  cdlemc5  40174  cdlemd3  40179  cdleme3g  40213  cdleme3h  40214  cdleme7d  40225  cdleme11c  40240  cdleme11k  40247  cdleme15d  40256  cdleme16e  40261  cdleme16f  40262  cdleme17b  40266  cdlemednpq  40278  cdleme19a  40282  cdleme20j  40297  cdleme21c  40306  cdleme22aa  40318  cdleme22b  40320  cdleme22cN  40321  cdleme22d  40322  cdleme23c  40330  cdleme28a  40349  cdleme35a  40427  cdleme35b  40429  cdleme35f  40433  cdleme42i  40462  cdlemeg46req  40508  cdlemf2  40541  cdlemg4c  40591  cdlemg6c  40599  cdlemg8b  40607  cdlemg10  40620  cdlemg11b  40621  cdlemg12f  40627  cdlemg13a  40630  cdlemg17a  40640  cdlemg17dALTN  40643  cdlemg18b  40658  cdlemg19a  40662  cdlemg27a  40671  cdlemg33b0  40680  cdlemg35  40692  cdlemg42  40708  cdlemg46  40714  trljco  40719  tendopltp  40759  cdlemi  40799  cdlemk3  40812  cdlemk10  40822  cdlemk15  40834  cdlemk1u  40838  cdlemk39  40895  cdlemk50  40931  erng1lem  40966  erngdvlem4  40970  erngdvlem4-rN  40978  dialss  41025  dia2dimlem1  41043  dia2dimlem10  41052  dia2dimlem12  41054  cdlemm10N  41097  djajN  41116  diblss  41149  cdlemn2  41174  dihjustlem  41195  dihord1  41197  dihord2pre2  41205  dib2dim  41222  dih2dimb  41223  dih2dimbALTN  41224  dihopelvalcpre  41227  dihord5b  41238  dihord5apre  41241  dihmeetlem1N  41269  dihglblem5apreN  41270  dihglblem2N  41273  dihmeetlem2N  41278  dihmeetlem3N  41284  lclkrlem2f  41491  lclkrlem2v  41507  lclkrslem2  41517  lcfrlem25  41546  lcfrlem35  41556  mapdlsm  41643  evlsval3  42532  disjinfi  45170  fourierdlem54  46142  fourierdlem76  46164  uhgrimisgrgriclem  47914