Theorem mpbir3and 1341

Description: Detach a conjunction of truths in a biconditional. (Contributed by Mario Carneiro, 11-May-2014.) (Revised by Mario Carneiro, 9-Jan-2015.)

Hypotheses

Ref	Expression
mpbir3and.1	⊢ (𝜑 → 𝜒)
mpbir3and.2	⊢ (𝜑 → 𝜃)
mpbir3and.3	⊢ (𝜑 → 𝜏)
mpbir3and.4	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))

Assertion

Ref	Expression
mpbir3and	⊢ (𝜑 → 𝜓)

Proof of Theorem mpbir3and

Step	Hyp	Ref	Expression
1		mpbir3and.1	. . 3 ⊢ (𝜑 → 𝜒)
2		mpbir3and.2	. . 3 ⊢ (𝜑 → 𝜃)
3		mpbir3and.3	. . 3 ⊢ (𝜑 → 𝜏)
4	1, 2, 3	3jca 1127	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
5		mpbir3and.4	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))
6	4, 5	mpbird 256	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  2ellim  8316  canthwelem  10416  intwun  10501  tskwun  10550  gruwun  10579  ixxss1  13107  ixxss2  13108  ixxss12  13109  ixxub  13110  ixxlb  13111  elicod  13139  ubioc1  13142  lbico1  13143  lbicc2  13206  ubicc2  13207  difreicc  13226  supicc  13243  modelico  13611  zmodfz  13623  addmodid  13649  dfrtrcl2  14783  phicl2  16479  4sqlem12  16667  isfuncd  17590  idfucl  17606  cofucl  17613  invfuc  17702  cnvps  18306  psss  18308  issubmd  18455  mndissubm  18456  submid  18459  subsubm  18465  0subm  18466  mhmima  18473  mhmeql  18474  gsumwspan  18495  frmdsssubm  18510  sursubmefmnd  18545  injsubmefmnd  18546  issubgrpd2  18781  grpissubg  18785  subgint  18789  0subg  18790  nmzsubg  18803  eqger  18816  eqgcpbl  18820  cycsubm  18831  cycsubgcl  18835  ghmrn  18857  ghmpreima  18866  gastacl  18925  cntzsubm  18952  sylow2blem1  19235  lsmsubm  19268  torsubg  19465  oddvdssubg  19466  dmdprdd  19612  dprdsubg  19637  dprdres  19641  unitsubm  19922  subrgsubm  20047  subrgugrp  20053  subrgint  20056  issubdrg  20059  cntzsubr  20067  lsssubg  20229  islmhm2  20310  pj1lmhm  20372  islbs2  20426  islbs3  20427  lbsextlem4  20433  issubrngd2  20469  lidlsubg  20496  2idlcpbl  20515  isphld  20869  mplsubglem  21215  mplsubrg  21221  mplind  21288  mhpsubg  21353  dmatsgrp  21658  dmatsrng  21660  scmatsgrp  21678  scmatsrng  21679  scmatsgrp1  21681  scmatsrng1  21682  cpmatsubgpmat  21879  cpmatsrgpmat  21880  lmcnp  22465  isufil2  23069  ufileu  23080  filufint  23081  fmfnfm  23119  flimclslem  23145  fclsfnflim  23188  flimfnfcls  23189  fclscmp  23191  clssubg  23270  tgpconncompeqg  23273  tgpconncomp  23274  qustgpopn  23281  tgptsmscls  23311  xmeter  23596  metust  23724  tgqioo  23973  zcld  23986  iccntr  23994  icccmplem2  23996  icccmplem3  23997  reconnlem1  23999  reconnlem2  24000  xrge0tsms  24007  cnheiborlem  24127  om1addcl  24206  pi1blem  24212  pi1grplem  24222  pi1inv  24225  pi1xfr  24228  pi1xfrcnvlem  24229  pi1coghm  24234  cmetcaulem  24462  ivthlem2  24626  ivthlem3  24627  ovolicc2lem2  24692  ovolicc2lem5  24695  opnmbllem  24775  volcn  24780  ismbf3d  24828  mbfi1fseqlem6  24895  itg2const2  24916  i1fibl  24982  ibladd  24995  bddiblnc  25016  ditgsplitlem  25034  dvferm1lem  25158  dvferm2lem  25160  dvlip2  25169  dvivthlem1  25182  dvne0  25185  lhop1lem  25187  lhop1  25188  lhop  25190  dvcnvrelem1  25191  dvcnvrelem2  25192  dvcnvre  25193  ftc1lem1  25209  itgsubst  25223  aaliou3lem2  25513  psercnlem2  25593  efif1olem2  25709  logtayl  25825  log2tlbnd  26105  xrlimcnp  26128  pntibndlem2  26749  pntlemj  26761  pntleml  26769  trgcgr  26887  hlid  26980  hltr  26981  btwnhl1  26983  btwnhl2  26984  hlcgrex  26987  mirhl  27050  mirbtwnhl  27051  mirhl2  27052  hlpasch  27127  lnopp2hpgb  27134  cgrahl  27198  axlowdim  27339  uhgrissubgr  27652  egrsubgr  27654  uhgrspansubgr  27668  uhgrspan1  27680  cusgrrusgr  27958  wlkonwlk  28039  wlkonwlk1l  28040  wlkres  28047  wlkp1  28058  wlkd  28063  lfgriswlk  28065  wwlksnextinj  28272  2wlkond  28310  wpthswwlks2on  28334  0wlkon  28492  1wlkd  28513  1pthond  28516  eliccelico  31106  elicoelioo  31107  xrge0tsmsd  31325  tpr2rico  31870  measinb  32197  cntmeas  32202  dya2icoseg  32252  sibf0  32309  sibfof  32315  pfxwlk  33093  revwlk  33094  resconn  33216  cvmsss2  33244  cvmliftlem10  33264  mrsubco  33491  bday0b  34032  madebdaylemlrcut  34087  cofcut1  34098  cgrextend  34318  cgr3rflx  34364  cgrxfr  34365  btwnconn1lem4  34400  btwnconn1lem8  34404  btwnconn1lem11  34407  bj-pinftynminfty  35406  bj-rveccmod  35481  iooelexlt  35541  opnmbllem0  35821  ibladdnc  35842  ftc1anc  35866  isbnd3  35950  prdsbnd  35959  rngomndo  36101  isgrpda  36121  rngohomco  36140  rngoisocnv  36147  rngoidl  36190  0idl  36191  intidl  36195  unichnidl  36197  keridl  36198  smprngopr  36218  lshpnel2N  37007  lkrshp  37127  4atexlemex2  38093  4atex  38098  cdleme0moN  38247  istendod  38784  dihlspsnat  39355  dochsatshp  39473  mon1psubm  41039  iocinico  41051  dfrtrcl3  41322  eliood  43017  eliccd  43023  eliocd  43026  limciccioolb  43143  limcicciooub  43159  icccncfext  43409  iblspltprt  43495  itgspltprt  43501  fourierdlem1  43630  fourierdlem4  43633  fourierdlem32  43661  fourierdlem33  43662  fourierdlem43  43672  fourierdlem65  43693  fourierdlem79  43707  prsal  43840  issald  43853  iccpartrn  44860  fpprwpprb  45170  bgoldbtbnd  45239  expnegico01  45837  dignnld  45927  reorelicc  46034