Theorem mpbi2and 719

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397

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 209  df-an 398

This theorem is referenced by:  supiso  9383  hartogslem1  9451  cantnfp1lem3  9596  oemapwe  9610  cantnffval2  9611  mulne0d  11797  flflp1  13761  flval2  13768  remim  15074  ntrivcvgtail  15860  divalgmod  16370  divnumden  16713  numdensq  16719  numdenexp  16725  prmdivdiv  16752  4sqlem7  16910  isposd  18283  poslubmo  18370  posglbmo  18371  latasymd  18406  latjidm  18423  latmidm  18435  latledi  18438  latjass  18444  mod1ile  18454  isglbd  18470  lubun  18476  ismgmid2  18631  oppginv  19329  slwhash  19594  lsmmod  19645  iscmnd  19764  dprd2da  20014  dmdprdsplit2lem  20017  dprdsplit  20020  pgpfac1lem1  20046  ringurd  20161  imasring  20305  subrg1  20558  isdrngd  20741  isdrngdOLD  20743  lsmsp  21080  lspprabs  21089  lsmcv  21138  psr1  21949  evlsval3  22069  mat1  22434  lmcn2  23636  dvdsq1p  26150  wilthlem2  27054  dchr1  27242  ismir  28749  vdgfrgrgt2  30390  atcvatlem  32478  ressprs  33049  rprmasso  33620  rprmasso3  33622  zarclssn  34069  ordtconnlem1  34120  cvmliftphtlem  35560  cvmlift3lem6  35567  cvmlift3lem9  35570  poimirlem13  38015  poimirlem14  38016  lsatexch  39550  lsatcvatlem  39556  oldmm1  39724  olj01  39732  olm01  39743  cvrcmp  39790  atcvreq0  39821  cvlexchb1  39837  cvlcvr1  39846  exatleN  39911  hlrelat3  39919  cvrval3  39920  cvratlem  39928  atlelt  39945  cvrat3  39949  2atjm  39952  atbtwn  39953  hlatexch3N  39987  hlatexch4  39988  2llnmat  40031  2atm  40034  lplnexllnN  40071  2llnjaN  40073  4atlem11b  40115  4atlem12b  40118  2lplnja  40126  dalem1  40166  dalemcea  40167  dalem3  40171  dalem8  40177  dalem16  40186  dalem17  40187  dalem21  40201  dalem25  40205  dalem39  40218  dalem54  40233  dalem55  40234  dalem57  40236  dalem60  40239  2lnat  40291  2atm2atN  40292  2llnma1b  40293  cdlema1N  40298  paddasslem12  40338  paddasslem13  40339  pmodlem1  40353  dalawlem2  40379  dalawlem3  40380  dalawlem5  40382  dalawlem6  40383  dalawlem8  40385  dalawlem11  40388  dalawlem12  40389  osumcllem1N  40463  lhp2lt  40508  lhpexle2lem  40516  lhpexle3lem  40518  lhpocnle  40523  lhpat3  40553  4atexlemtlw  40574  4atexlemnclw  40577  4atexlemcnd  40579  lautj  40600  lautm  40601  trlval3  40694  cdlemc5  40702  cdlemd3  40707  cdleme3g  40741  cdleme3h  40742  cdleme7d  40753  cdleme11c  40768  cdleme11k  40775  cdleme15d  40784  cdleme16e  40789  cdleme16f  40790  cdleme17b  40794  cdlemednpq  40806  cdleme19a  40810  cdleme20j  40825  cdleme21c  40834  cdleme22aa  40846  cdleme22b  40848  cdleme22cN  40849  cdleme22d  40850  cdleme23c  40858  cdleme28a  40877  cdleme35a  40955  cdleme35b  40957  cdleme35f  40961  cdleme42i  40990  cdlemeg46req  41036  cdlemf2  41069  cdlemg4c  41119  cdlemg6c  41127  cdlemg8b  41135  cdlemg10  41148  cdlemg11b  41149  cdlemg12f  41155  cdlemg13a  41158  cdlemg17a  41168  cdlemg17dALTN  41171  cdlemg18b  41186  cdlemg19a  41190  cdlemg27a  41199  cdlemg33b0  41208  cdlemg35  41220  cdlemg42  41236  cdlemg46  41242  trljco  41247  tendopltp  41287  cdlemi  41327  cdlemk3  41340  cdlemk10  41350  cdlemk15  41362  cdlemk1u  41366  cdlemk39  41423  cdlemk50  41459  erng1lem  41494  erngdvlem4  41498  erngdvlem4-rN  41506  dialss  41553  dia2dimlem1  41571  dia2dimlem10  41580  dia2dimlem12  41582  cdlemm10N  41625  djajN  41644  diblss  41677  cdlemn2  41702  dihjustlem  41723  dihord1  41725  dihord2pre2  41733  dib2dim  41750  dih2dimb  41751  dih2dimbALTN  41752  dihopelvalcpre  41755  dihord5b  41766  dihord5apre  41769  dihmeetlem1N  41797  dihglblem5apreN  41798  dihglblem2N  41801  dihmeetlem2N  41806  dihmeetlem3N  41812  lclkrlem2f  42019  lclkrlem2v  42035  lclkrslem2  42045  lcfrlem25  42074  lcfrlem35  42084  mapdlsm  42171  disjinfi  45653  fourierdlem54  46617  fourierdlem76  46639  uhgrimisgrgriclem  48435