Theorem mpbi2and 722

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

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

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 400

This theorem is referenced by:  supiso  9419  hartogslem1  9487  cantnfp1lem3  9632  oemapwe  9646  cantnffval2  9647  mulne0d  11836  flflp1  13814  flval2  13821  remim  15127  ntrivcvgtail  15913  divalgmod  16423  divnumden  16766  numdensq  16772  numdenexp  16778  prmdivdiv  16805  4sqlem7  16963  isposd  18337  poslubmo  18424  posglbmo  18425  latasymd  18460  latjidm  18477  latmidm  18489  latledi  18492  latjass  18498  mod1ile  18508  isglbd  18524  lubun  18530  ismgmid2  18685  oppginv  19382  slwhash  19647  lsmmod  19698  iscmnd  19817  dprd2da  20067  dmdprdsplit2lem  20070  dprdsplit  20073  pgpfac1lem1  20099  ringurd  20214  imasring  20358  subrg1  20611  isdrngd  20794  isdrngdOLD  20796  lsmsp  21133  lspprabs  21142  lsmcv  21191  psr1  22002  evlsval3  22122  mat1  22487  lmcn2  23689  dvdsq1p  26203  wilthlem2  27110  dchr1  27298  ismir  28805  vdgfrgrgt2  30446  atcvatlem  32534  ressprs  33105  rprmasso  33682  rprmasso3  33684  zarclssn  34131  ordtconnlem1  34182  cvmliftphtlem  35631  cvmlift3lem6  35638  cvmlift3lem9  35641  poimirlem13  38096  poimirlem14  38097  lsatexch  39631  lsatcvatlem  39637  oldmm1  39805  olj01  39813  olm01  39824  cvrcmp  39871  atcvreq0  39902  cvlexchb1  39918  cvlcvr1  39927  exatleN  39992  hlrelat3  40000  cvrval3  40001  cvratlem  40009  atlelt  40026  cvrat3  40030  2atjm  40033  atbtwn  40034  hlatexch3N  40068  hlatexch4  40069  2llnmat  40112  2atm  40115  lplnexllnN  40152  2llnjaN  40154  4atlem11b  40196  4atlem12b  40199  2lplnja  40207  dalem1  40247  dalemcea  40248  dalem3  40252  dalem8  40258  dalem16  40267  dalem17  40268  dalem21  40282  dalem25  40286  dalem39  40299  dalem54  40314  dalem55  40315  dalem57  40317  dalem60  40320  2lnat  40372  2atm2atN  40373  2llnma1b  40374  cdlema1N  40379  paddasslem12  40419  paddasslem13  40420  pmodlem1  40434  dalawlem2  40460  dalawlem3  40461  dalawlem5  40463  dalawlem6  40464  dalawlem8  40466  dalawlem11  40469  dalawlem12  40470  osumcllem1N  40544  lhp2lt  40589  lhpexle2lem  40597  lhpexle3lem  40599  lhpocnle  40604  lhpat3  40634  4atexlemtlw  40655  4atexlemnclw  40658  4atexlemcnd  40660  lautj  40681  lautm  40682  trlval3  40775  cdlemc5  40783  cdlemd3  40788  cdleme3g  40822  cdleme3h  40823  cdleme7d  40834  cdleme11c  40849  cdleme11k  40856  cdleme15d  40865  cdleme16e  40870  cdleme16f  40871  cdleme17b  40875  cdlemednpq  40887  cdleme19a  40891  cdleme20j  40906  cdleme21c  40915  cdleme22aa  40927  cdleme22b  40929  cdleme22cN  40930  cdleme22d  40931  cdleme23c  40939  cdleme28a  40958  cdleme35a  41036  cdleme35b  41038  cdleme35f  41042  cdleme42i  41071  cdlemeg46req  41117  cdlemf2  41150  cdlemg4c  41200  cdlemg6c  41208  cdlemg8b  41216  cdlemg10  41229  cdlemg11b  41230  cdlemg12f  41236  cdlemg13a  41239  cdlemg17a  41249  cdlemg17dALTN  41252  cdlemg18b  41267  cdlemg19a  41271  cdlemg27a  41280  cdlemg33b0  41289  cdlemg35  41301  cdlemg42  41317  cdlemg46  41323  trljco  41328  tendopltp  41368  cdlemi  41408  cdlemk3  41421  cdlemk10  41431  cdlemk15  41443  cdlemk1u  41447  cdlemk39  41504  cdlemk50  41540  erng1lem  41575  erngdvlem4  41579  erngdvlem4-rN  41587  dialss  41634  dia2dimlem1  41652  dia2dimlem10  41661  dia2dimlem12  41663  cdlemm10N  41706  djajN  41725  diblss  41758  cdlemn2  41783  dihjustlem  41804  dihord1  41806  dihord2pre2  41814  dib2dim  41831  dih2dimb  41832  dih2dimbALTN  41833  dihopelvalcpre  41836  dihord5b  41847  dihord5apre  41850  dihmeetlem1N  41878  dihglblem5apreN  41879  dihglblem2N  41882  dihmeetlem2N  41887  dihmeetlem3N  41893  lclkrlem2f  42100  lclkrlem2v  42116  lclkrslem2  42126  lcfrlem25  42155  lcfrlem35  42165  mapdlsm  42252  disjinfi  45734  fourierdlem54  46698  fourierdlem76  46720  uhgrimisgrgriclem  48516