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  9498  hartogslem1  9565  cantnfp1lem3  9703  oemapwe  9717  cantnffval2  9718  mulne0d  11898  flflp1  13830  flval2  13837  remim  15139  ntrivcvgtail  15919  divalgmod  16426  divnumden  16768  numdensq  16774  numdenexp  16780  prmdivdiv  16807  4sqlem7  16965  isposd  18343  poslubmo  18430  posglbmo  18431  latasymd  18464  latjidm  18481  latmidm  18493  latledi  18496  latjass  18502  mod1ile  18512  isglbd  18528  lubun  18534  ismgmid2  18655  oppginv  19351  slwhash  19615  lsmmod  19666  iscmnd  19785  dprd2da  20035  dmdprdsplit2lem  20038  dprdsplit  20041  pgpfac1lem1  20067  ringurd  20155  imasring  20300  subrg1  20555  isdrngd  20738  isdrngdOLD  20740  lsmsp  21058  lspprabs  21067  lsmcv  21116  psr1  21958  mat1  22420  lmcn2  23622  dvdsq1p  26157  wilthlem2  27067  dchr1  27256  ismir  28622  vdgfrgrgt2  30264  atcvatlem  32351  ressprs  32900  rprmasso  33494  rprmasso3  33496  zarclssn  33813  ordtconnlem1  33864  cvmliftphtlem  35263  cvmlift3lem6  35270  cvmlift3lem9  35273  poimirlem13  37581  poimirlem14  37582  lsatexch  38985  lsatcvatlem  38991  oldmm1  39159  olj01  39167  olm01  39178  cvrcmp  39225  atcvreq0  39256  cvlexchb1  39272  cvlcvr1  39281  exatleN  39347  hlrelat3  39355  cvrval3  39356  cvratlem  39364  atlelt  39381  cvrat3  39385  2atjm  39388  atbtwn  39389  hlatexch3N  39423  hlatexch4  39424  2llnmat  39467  2atm  39470  lplnexllnN  39507  2llnjaN  39509  4atlem11b  39551  4atlem12b  39554  2lplnja  39562  dalem1  39602  dalemcea  39603  dalem3  39607  dalem8  39613  dalem16  39622  dalem17  39623  dalem21  39637  dalem25  39641  dalem39  39654  dalem54  39669  dalem55  39670  dalem57  39672  dalem60  39675  2lnat  39727  2atm2atN  39728  2llnma1b  39729  cdlema1N  39734  paddasslem12  39774  paddasslem13  39775  pmodlem1  39789  dalawlem2  39815  dalawlem3  39816  dalawlem5  39818  dalawlem6  39819  dalawlem8  39821  dalawlem11  39824  dalawlem12  39825  osumcllem1N  39899  lhp2lt  39944  lhpexle2lem  39952  lhpexle3lem  39954  lhpocnle  39959  lhpat3  39989  4atexlemtlw  40010  4atexlemnclw  40013  4atexlemcnd  40015  lautj  40036  lautm  40037  trlval3  40130  cdlemc5  40138  cdlemd3  40143  cdleme3g  40177  cdleme3h  40178  cdleme7d  40189  cdleme11c  40204  cdleme11k  40211  cdleme15d  40220  cdleme16e  40225  cdleme16f  40226  cdleme17b  40230  cdlemednpq  40242  cdleme19a  40246  cdleme20j  40261  cdleme21c  40270  cdleme22aa  40282  cdleme22b  40284  cdleme22cN  40285  cdleme22d  40286  cdleme23c  40294  cdleme28a  40313  cdleme35a  40391  cdleme35b  40393  cdleme35f  40397  cdleme42i  40426  cdlemeg46req  40472  cdlemf2  40505  cdlemg4c  40555  cdlemg6c  40563  cdlemg8b  40571  cdlemg10  40584  cdlemg11b  40585  cdlemg12f  40591  cdlemg13a  40594  cdlemg17a  40604  cdlemg17dALTN  40607  cdlemg18b  40622  cdlemg19a  40626  cdlemg27a  40635  cdlemg33b0  40644  cdlemg35  40656  cdlemg42  40672  cdlemg46  40678  trljco  40683  tendopltp  40723  cdlemi  40763  cdlemk3  40776  cdlemk10  40786  cdlemk15  40798  cdlemk1u  40802  cdlemk39  40859  cdlemk50  40895  erng1lem  40930  erngdvlem4  40934  erngdvlem4-rN  40942  dialss  40989  dia2dimlem1  41007  dia2dimlem10  41016  dia2dimlem12  41018  cdlemm10N  41061  djajN  41080  diblss  41113  cdlemn2  41138  dihjustlem  41159  dihord1  41161  dihord2pre2  41169  dib2dim  41186  dih2dimb  41187  dih2dimbALTN  41188  dihopelvalcpre  41191  dihord5b  41202  dihord5apre  41205  dihmeetlem1N  41233  dihglblem5apreN  41234  dihglblem2N  41237  dihmeetlem2N  41242  dihmeetlem3N  41248  lclkrlem2f  41455  lclkrlem2v  41471  lclkrslem2  41481  lcfrlem25  41510  lcfrlem35  41520  mapdlsm  41607  evlsval3  42514  disjinfi  45142  fourierdlem54  46120  fourierdlem76  46142  uhgrimisgrgriclem  47844