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  9427  hartogslem1  9495  cantnfp1lem3  9633  oemapwe  9647  cantnffval2  9648  mulne0d  11830  flflp1  13769  flval2  13776  remim  15083  ntrivcvgtail  15866  divalgmod  16376  divnumden  16718  numdensq  16724  numdenexp  16730  prmdivdiv  16757  4sqlem7  16915  isposd  18283  poslubmo  18370  posglbmo  18371  latasymd  18404  latjidm  18421  latmidm  18433  latledi  18436  latjass  18442  mod1ile  18452  isglbd  18468  lubun  18474  ismgmid2  18595  oppginv  19291  slwhash  19554  lsmmod  19605  iscmnd  19724  dprd2da  19974  dmdprdsplit2lem  19977  dprdsplit  19980  pgpfac1lem1  20006  ringurd  20094  imasring  20239  subrg1  20491  isdrngd  20674  isdrngdOLD  20676  lsmsp  20993  lspprabs  21002  lsmcv  21051  psr1  21880  mat1  22334  lmcn2  23536  dvdsq1p  26068  wilthlem2  26979  dchr1  27168  ismir  28586  vdgfrgrgt2  30227  atcvatlem  32314  ressprs  32890  rprmasso  33496  rprmasso3  33498  zarclssn  33863  ordtconnlem1  33914  cvmliftphtlem  35304  cvmlift3lem6  35311  cvmlift3lem9  35314  poimirlem13  37627  poimirlem14  37628  lsatexch  39036  lsatcvatlem  39042  oldmm1  39210  olj01  39218  olm01  39229  cvrcmp  39276  atcvreq0  39307  cvlexchb1  39323  cvlcvr1  39332  exatleN  39398  hlrelat3  39406  cvrval3  39407  cvratlem  39415  atlelt  39432  cvrat3  39436  2atjm  39439  atbtwn  39440  hlatexch3N  39474  hlatexch4  39475  2llnmat  39518  2atm  39521  lplnexllnN  39558  2llnjaN  39560  4atlem11b  39602  4atlem12b  39605  2lplnja  39613  dalem1  39653  dalemcea  39654  dalem3  39658  dalem8  39664  dalem16  39673  dalem17  39674  dalem21  39688  dalem25  39692  dalem39  39705  dalem54  39720  dalem55  39721  dalem57  39723  dalem60  39726  2lnat  39778  2atm2atN  39779  2llnma1b  39780  cdlema1N  39785  paddasslem12  39825  paddasslem13  39826  pmodlem1  39840  dalawlem2  39866  dalawlem3  39867  dalawlem5  39869  dalawlem6  39870  dalawlem8  39872  dalawlem11  39875  dalawlem12  39876  osumcllem1N  39950  lhp2lt  39995  lhpexle2lem  40003  lhpexle3lem  40005  lhpocnle  40010  lhpat3  40040  4atexlemtlw  40061  4atexlemnclw  40064  4atexlemcnd  40066  lautj  40087  lautm  40088  trlval3  40181  cdlemc5  40189  cdlemd3  40194  cdleme3g  40228  cdleme3h  40229  cdleme7d  40240  cdleme11c  40255  cdleme11k  40262  cdleme15d  40271  cdleme16e  40276  cdleme16f  40277  cdleme17b  40281  cdlemednpq  40293  cdleme19a  40297  cdleme20j  40312  cdleme21c  40321  cdleme22aa  40333  cdleme22b  40335  cdleme22cN  40336  cdleme22d  40337  cdleme23c  40345  cdleme28a  40364  cdleme35a  40442  cdleme35b  40444  cdleme35f  40448  cdleme42i  40477  cdlemeg46req  40523  cdlemf2  40556  cdlemg4c  40606  cdlemg6c  40614  cdlemg8b  40622  cdlemg10  40635  cdlemg11b  40636  cdlemg12f  40642  cdlemg13a  40645  cdlemg17a  40655  cdlemg17dALTN  40658  cdlemg18b  40673  cdlemg19a  40677  cdlemg27a  40686  cdlemg33b0  40695  cdlemg35  40707  cdlemg42  40723  cdlemg46  40729  trljco  40734  tendopltp  40774  cdlemi  40814  cdlemk3  40827  cdlemk10  40837  cdlemk15  40849  cdlemk1u  40853  cdlemk39  40910  cdlemk50  40946  erng1lem  40981  erngdvlem4  40985  erngdvlem4-rN  40993  dialss  41040  dia2dimlem1  41058  dia2dimlem10  41067  dia2dimlem12  41069  cdlemm10N  41112  djajN  41131  diblss  41164  cdlemn2  41189  dihjustlem  41210  dihord1  41212  dihord2pre2  41220  dib2dim  41237  dih2dimb  41238  dih2dimbALTN  41239  dihopelvalcpre  41242  dihord5b  41253  dihord5apre  41256  dihmeetlem1N  41284  dihglblem5apreN  41285  dihglblem2N  41288  dihmeetlem2N  41293  dihmeetlem3N  41299  lclkrlem2f  41506  lclkrlem2v  41522  lclkrslem2  41532  lcfrlem25  41561  lcfrlem35  41571  mapdlsm  41658  evlsval3  42547  disjinfi  45186  fourierdlem54  46158  fourierdlem76  46180  uhgrimisgrgriclem  47930