Theorem mpbi2and 724

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  supiso  9437  hartogslem1  9505  cantnfp1lem3  9650  oemapwe  9664  cantnffval2  9665  mulne0d  11867  flflp1  13842  flval2  13849  remim  15170  ntrivcvgtail  15956  divalgmod  16465  divnumden  16808  numdensq  16814  numdenexp  16820  prmdivdiv  16847  4sqlem7  17005  isposd  18379  poslubmo  18466  posglbmo  18467  latasymd  18502  latjidm  18519  latmidm  18531  latledi  18534  latjass  18540  mod1ile  18550  isglbd  18566  lubun  18572  ismgmid2  18727  oppginv  19430  slwhash  19695  lsmmod  19746  iscmnd  19865  dprd2da  20115  dmdprdsplit2lem  20118  dprdsplit  20121  pgpfac1lem1  20147  ringurd  20268  imasring  20413  subrg1  20668  isdrngd  20850  isdrngdOLD  20852  lsmsp  21188  lspprabs  21197  lsmcv  21246  psr1  22101  evlsval3  22221  mat1  22585  lmcn2  23787  dvdsq1p  26301  wilthlem2  27211  dchr1  27399  ismir  28914  vdgfrgrgt2  30627  atcvatlem  32715  ressprs  33264  rprmasso  33793  rprmasso3  33795  zarclssn  34241  ordtconnlem1  34292  cvmliftphtlem  35787  cvmlift3lem6  35794  cvmlift3lem9  35797  poimirlem13  38262  poimirlem14  38263  lsatexch  39795  lsatcvatlem  39801  oldmm1  39969  olj01  39977  olm01  39988  cvrcmp  40035  atcvreq0  40066  cvlexchb1  40082  cvlcvr1  40091  exatleN  40156  hlrelat3  40164  cvrval3  40165  cvratlem  40173  atlelt  40190  cvrat3  40194  2atjm  40197  atbtwn  40198  hlatexch3N  40232  hlatexch4  40233  2llnmat  40276  2atm  40279  lplnexllnN  40316  2llnjaN  40318  4atlem11b  40360  4atlem12b  40363  2lplnja  40371  dalem1  40411  dalemcea  40412  dalem3  40416  dalem8  40422  dalem16  40431  dalem17  40432  dalem21  40446  dalem25  40450  dalem39  40463  dalem54  40478  dalem55  40479  dalem57  40481  dalem60  40484  2lnat  40536  2atm2atN  40537  2llnma1b  40538  cdlema1N  40543  paddasslem12  40583  paddasslem13  40584  pmodlem1  40598  dalawlem2  40624  dalawlem3  40625  dalawlem5  40627  dalawlem6  40628  dalawlem8  40630  dalawlem11  40633  dalawlem12  40634  osumcllem1N  40708  lhp2lt  40753  lhpexle2lem  40761  lhpexle3lem  40763  lhpocnle  40768  lhpat3  40798  4atexlemtlw  40819  4atexlemnclw  40822  4atexlemcnd  40824  lautj  40845  lautm  40846  trlval3  40939  cdlemc5  40947  cdlemd3  40952  cdleme3g  40986  cdleme3h  40987  cdleme7d  40998  cdleme11c  41013  cdleme11k  41020  cdleme15d  41029  cdleme16e  41034  cdleme16f  41035  cdleme17b  41039  cdlemednpq  41051  cdleme19a  41055  cdleme20j  41070  cdleme21c  41079  cdleme22aa  41091  cdleme22b  41093  cdleme22cN  41094  cdleme22d  41095  cdleme23c  41103  cdleme28a  41122  cdleme35a  41200  cdleme35b  41202  cdleme35f  41206  cdleme42i  41235  cdlemeg46req  41281  cdlemf2  41314  cdlemg4c  41364  cdlemg6c  41372  cdlemg8b  41380  cdlemg10  41393  cdlemg11b  41394  cdlemg12f  41400  cdlemg13a  41403  cdlemg17a  41413  cdlemg17dALTN  41416  cdlemg18b  41431  cdlemg19a  41435  cdlemg27a  41444  cdlemg33b0  41453  cdlemg35  41465  cdlemg42  41481  cdlemg46  41487  trljco  41492  tendopltp  41532  cdlemi  41572  cdlemk3  41585  cdlemk10  41595  cdlemk15  41607  cdlemk1u  41611  cdlemk39  41668  cdlemk50  41704  erng1lem  41739  erngdvlem4  41743  erngdvlem4-rN  41751  dialss  41798  dia2dimlem1  41816  dia2dimlem10  41825  dia2dimlem12  41827  cdlemm10N  41870  djajN  41889  diblss  41922  cdlemn2  41947  dihjustlem  41968  dihord1  41970  dihord2pre2  41978  dib2dim  41995  dih2dimb  41996  dih2dimbALTN  41997  dihopelvalcpre  42000  dihord5b  42011  dihord5apre  42014  dihmeetlem1N  42042  dihglblem5apreN  42043  dihglblem2N  42046  dihmeetlem2N  42051  dihmeetlem3N  42057  lclkrlem2f  42264  lclkrlem2v  42280  lclkrslem2  42290  lcfrlem25  42319  lcfrlem35  42329  mapdlsm  42416  disjinfi  45890  fourierdlem54  46854  fourierdlem76  46876  uhgrimisgrgriclem  48672