Theorem mpbir3and 1342

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 1128	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
5		mpbir3and.4	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))
6	4, 5	mpbird 256	1 ⊢ (𝜑 → 𝜓)

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

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 1089

This theorem is referenced by:  2ellim  8501  canthwelem  10647  intwun  10732  tskwun  10781  gruwun  10810  ixxss1  13344  ixxss2  13345  ixxss12  13346  ixxub  13347  ixxlb  13348  elicod  13376  ubioc1  13379  lbico1  13380  lbicc2  13443  ubicc2  13444  difreicc  13463  supicc  13480  modelico  13848  zmodfz  13860  addmodid  13886  dfrtrcl2  15011  phicl2  16703  4sqlem12  16891  isfuncd  17817  idfucl  17833  cofucl  17840  invfuc  17929  cnvps  18533  psss  18535  issubmd  18689  mndissubm  18690  submid  18693  subsubm  18699  0subm  18700  mhmima  18708  mhmeql  18709  gsumwspan  18729  frmdsssubm  18744  sursubmefmnd  18779  injsubmefmnd  18780  issubgrpd2  19024  grpissubg  19028  subgint  19032  0subgOLD  19034  nmzsubg  19047  eqger  19060  eqgcpbl  19064  cycsubm  19081  cycsubgcl  19085  ghmrn  19107  ghmpreima  19116  gastacl  19175  cntzsubm  19204  sylow2blem1  19490  lsmsubm  19523  torsubg  19724  oddvdssubg  19725  dmdprdd  19871  dprdsubg  19896  dprdres  19900  unitsubm  20204  subrgsubm  20336  subrgugrp  20342  subrgint  20346  cntzsubr  20357  issubdrg  20405  lsssubg  20573  islmhm2  20654  pj1lmhm  20716  islbs2  20773  islbs3  20774  lbsextlem4  20780  issubrgd  20817  lidlsubg  20844  2idlcpbl  20877  isphld  21213  mplsubglem  21564  mplsubrg  21570  mplind  21637  mhpsubg  21702  dmatsgrp  22008  dmatsrng  22010  scmatsgrp  22028  scmatsrng  22029  scmatsgrp1  22031  scmatsrng1  22032  cpmatsubgpmat  22229  cpmatsrgpmat  22230  lmcnp  22815  isufil2  23419  ufileu  23430  filufint  23431  fmfnfm  23469  flimclslem  23495  fclsfnflim  23538  flimfnfcls  23539  fclscmp  23541  clssubg  23620  tgpconncompeqg  23623  tgpconncomp  23624  qustgpopn  23631  tgptsmscls  23661  xmeter  23946  metust  24074  tgqioo  24323  zcld  24336  iccntr  24344  icccmplem2  24346  icccmplem3  24347  reconnlem1  24349  reconnlem2  24350  xrge0tsms  24357  cnheiborlem  24477  om1addcl  24556  pi1blem  24562  pi1grplem  24572  pi1inv  24575  pi1xfr  24578  pi1xfrcnvlem  24579  pi1coghm  24584  cmetcaulem  24812  ivthlem2  24976  ivthlem3  24977  ovolicc2lem2  25042  ovolicc2lem5  25045  opnmbllem  25125  volcn  25130  ismbf3d  25178  mbfi1fseqlem6  25245  itg2const2  25266  i1fibl  25332  ibladd  25345  bddiblnc  25366  ditgsplitlem  25384  dvferm1lem  25508  dvferm2lem  25510  dvlip2  25519  dvivthlem1  25532  dvne0  25535  lhop1lem  25537  lhop1  25538  lhop  25540  dvcnvrelem1  25541  dvcnvrelem2  25542  dvcnvre  25543  ftc1lem1  25559  itgsubst  25573  aaliou3lem2  25863  psercnlem2  25943  efif1olem2  26059  logtayl  26175  log2tlbnd  26457  xrlimcnp  26480  pntibndlem2  27101  pntlemj  27113  pntleml  27121  bday0b  27339  cuteq0  27341  cuteq1  27342  madebdaylemlrcut  27401  cofcut1  27416  trgcgr  27805  hlid  27898  hltr  27899  btwnhl1  27901  btwnhl2  27902  hlcgrex  27905  mirhl  27968  mirbtwnhl  27969  mirhl2  27970  hlpasch  28045  lnopp2hpgb  28052  cgrahl  28116  axlowdim  28257  uhgrissubgr  28570  egrsubgr  28572  uhgrspansubgr  28586  uhgrspan1  28598  cusgrrusgr  28876  wlkonwlk  28957  wlkonwlk1l  28958  wlkres  28965  wlkp1  28976  wlkd  28981  lfgriswlk  28983  wwlksnextinj  29191  2wlkond  29229  wpthswwlks2on  29253  0wlkon  29411  1wlkd  29432  1pthond  29435  eliccelico  32026  elicoelioo  32027  xrge0tsmsd  32250  tpr2rico  32961  measinb  33288  cntmeas  33293  dya2icoseg  33345  sibf0  33402  sibfof  33408  pfxwlk  34183  revwlk  34184  resconn  34306  cvmsss2  34334  cvmliftlem10  34354  mrsubco  34581  cgrextend  35049  cgr3rflx  35095  cgrxfr  35096  btwnconn1lem4  35131  btwnconn1lem8  35135  btwnconn1lem11  35138  bj-pinftynminfty  36194  bj-rveccmod  36269  iooelexlt  36329  opnmbllem0  36610  ibladdnc  36631  ftc1anc  36655  isbnd3  36738  prdsbnd  36747  rngomndo  36889  isgrpda  36909  rngohomco  36928  rngoisocnv  36935  rngoidl  36978  0idl  36979  intidl  36983  unichnidl  36985  keridl  36986  smprngopr  37006  lshpnel2N  37941  lkrshp  38061  4atexlemex2  39028  4atex  39033  cdleme0moN  39182  istendod  39719  dihlspsnat  40290  dochsatshp  40408  mon1psubm  42030  iocinico  42043  dfrtrcl3  42566  eliood  44290  eliccd  44296  eliocd  44299  limciccioolb  44416  limcicciooub  44432  icccncfext  44682  iblspltprt  44768  itgspltprt  44774  fourierdlem1  44903  fourierdlem4  44906  fourierdlem32  44934  fourierdlem33  44935  fourierdlem43  44945  fourierdlem65  44966  fourierdlem79  44980  prsal  45113  issald  45128  iccpartrn  46177  fpprwpprb  46487  bgoldbtbnd  46556  cntzsubrng  46825  2idlcpblrng  46845  expnegico01  47277  dignnld  47367  reorelicc  47474