Theorem mpbir3and 1343

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 257	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  2ellim  8424  canthwelem  10563  intwun  10648  tskwun  10697  gruwun  10726  ixxss1  13284  ixxss2  13285  ixxss12  13286  ixxub  13287  ixxlb  13288  elicod  13316  ubioc1  13320  lbico1  13321  lbicc2  13385  ubicc2  13386  difreicc  13405  supicc  13422  modelico  13803  zmodfz  13815  addmodid  13844  dfrtrcl2  14987  phicl2  16697  4sqlem12  16886  isfuncd  17790  idfucl  17806  cofucl  17813  invfuc  17902  cnvps  18502  psss  18504  issubmd  18698  mndissubm  18699  submid  18702  subsubm  18708  0subm  18709  mhmima  18717  mhmeql  18718  gsumwspan  18738  frmdsssubm  18753  sursubmefmnd  18788  injsubmefmnd  18789  issubgrpd2  19039  grpissubg  19043  subgint  19047  0subgOLD  19049  nmzsubg  19062  eqger  19075  eqgcpbl  19079  cycsubm  19099  cycsubgcl  19103  ghmrn  19126  ghmpreima  19135  gastacl  19206  cntzsubm  19235  sylow2blem1  19517  lsmsubm  19550  torsubg  19751  oddvdssubg  19752  dmdprdd  19898  dprdsubg  19923  dprdres  19927  unitsubm  20289  cntzsubrng  20470  subrgsubm  20488  subrgugrp  20494  subrgint  20498  cntzsubr  20509  issubdrg  20683  lsssubg  20878  islmhm2  20960  pj1lmhm  21022  islbs2  21079  islbs3  21080  lbsextlem4  21086  issubrgd  21111  lidlsubg  21148  2idlcpblrng  21196  isphld  21579  mplsubglem  21924  mplsubrg  21930  mplind  21993  mhpsubg  22056  dmatsgrp  22402  dmatsrng  22404  scmatsgrp  22422  scmatsrng  22423  scmatsgrp1  22425  scmatsrng1  22426  cpmatsubgpmat  22623  cpmatsrgpmat  22624  lmcnp  23207  isufil2  23811  ufileu  23822  filufint  23823  fmfnfm  23861  flimclslem  23887  fclsfnflim  23930  flimfnfcls  23931  fclscmp  23933  clssubg  24012  tgpconncompeqg  24015  tgpconncomp  24016  qustgpopn  24023  tgptsmscls  24053  xmeter  24337  metust  24462  tgqioo  24704  zcld  24718  iccntr  24726  icccmplem2  24728  icccmplem3  24729  reconnlem1  24731  reconnlem2  24732  xrge0tsms  24739  cnheiborlem  24869  om1addcl  24949  pi1blem  24955  pi1grplem  24965  pi1inv  24968  pi1xfr  24971  pi1xfrcnvlem  24972  pi1coghm  24977  cmetcaulem  25204  ivthlem2  25369  ivthlem3  25370  ovolicc2lem2  25435  ovolicc2lem5  25438  opnmbllem  25518  volcn  25523  ismbf3d  25571  mbfi1fseqlem6  25637  itg2const2  25658  i1fibl  25725  ibladd  25738  bddiblnc  25759  ditgsplitlem  25777  dvferm1lem  25904  dvferm2lem  25906  dvlip2  25916  dvivthlem1  25929  dvne0  25932  lhop1lem  25934  lhop1  25935  lhop  25937  dvcnvrelem1  25938  dvcnvrelem2  25939  dvcnvre  25940  ftc1lem1  25958  itgsubst  25972  aaliou3lem2  26267  psercnlem2  26350  efif1olem2  26468  logtayl  26585  log2tlbnd  26871  xrlimcnp  26894  pntibndlem2  27518  pntlemj  27530  pntleml  27538  bday0b  27762  cuteq0  27764  cuteq1  27766  madebdaylemlrcut  27831  cofcut1  27851  onscutlt  28188  trgcgr  28479  hlid  28572  hltr  28573  btwnhl1  28575  btwnhl2  28576  hlcgrex  28579  mirhl  28642  mirbtwnhl  28643  mirhl2  28644  hlpasch  28719  lnopp2hpgb  28726  cgrahl  28790  axlowdim  28924  uhgrissubgr  29238  egrsubgr  29240  uhgrspansubgr  29254  uhgrspan1  29266  cusgrrusgr  29545  wlkonwlk  29624  wlkonwlk1l  29625  wlkres  29632  wlkp1  29643  wlkd  29648  lfgriswlk  29650  wwlksnextinj  29862  2wlkond  29900  wpthswwlks2on  29924  0wlkon  30082  1wlkd  30103  1pthond  30106  eliccelico  32733  elicoelioo  32734  xrge0tsmsd  33028  tpr2rico  33878  measinb  34187  cntmeas  34192  dya2icoseg  34244  sibf0  34301  sibfof  34307  pfxwlk  35096  revwlk  35097  resconn  35218  cvmsss2  35246  cvmliftlem10  35266  mrsubco  35493  cgrextend  35981  cgr3rflx  36027  cgrxfr  36028  btwnconn1lem4  36063  btwnconn1lem8  36067  btwnconn1lem11  36070  bj-pinftynminfty  37200  bj-rveccmod  37275  iooelexlt  37335  opnmbllem0  37635  ibladdnc  37656  ftc1anc  37680  isbnd3  37763  prdsbnd  37772  rngomndo  37914  isgrpda  37934  rngohomco  37953  rngoisocnv  37960  rngoidl  38003  0idl  38004  intidl  38008  unichnidl  38010  keridl  38011  smprngopr  38031  lshpnel2N  38963  lkrshp  39083  4atexlemex2  40050  4atex  40055  cdleme0moN  40204  istendod  40741  dihlspsnat  41312  dochsatshp  41430  mon1psubm  43172  iocinico  43185  dfrtrcl3  43706  eliood  45480  eliccd  45486  eliocd  45489  limciccioolb  45603  limcicciooub  45619  icccncfext  45869  iblspltprt  45955  itgspltprt  45961  fourierdlem1  46090  fourierdlem4  46093  fourierdlem32  46121  fourierdlem33  46122  fourierdlem43  46132  fourierdlem65  46153  fourierdlem79  46167  prsal  46300  issald  46315  iccpartrn  47415  fpprwpprb  47725  bgoldbtbnd  47794  upgrimwlk  47886  upgrimpths  47893  gpgedgvtx0  48036  gpgedgvtx1  48037  gpgprismgr4cycllem11  48079  expnegico01  48491  dignnld  48576  reorelicc  48683