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  8463  canthwelem  10603  intwun  10688  tskwun  10737  gruwun  10766  ixxss1  13324  ixxss2  13325  ixxss12  13326  ixxub  13327  ixxlb  13328  elicod  13356  ubioc1  13360  lbico1  13361  lbicc2  13425  ubicc2  13426  difreicc  13445  supicc  13462  modelico  13843  zmodfz  13855  addmodid  13884  dfrtrcl2  15028  phicl2  16738  4sqlem12  16927  isfuncd  17827  idfucl  17843  cofucl  17850  invfuc  17939  cnvps  18537  psss  18539  issubmd  18733  mndissubm  18734  submid  18737  subsubm  18743  0subm  18744  mhmima  18752  mhmeql  18753  gsumwspan  18773  frmdsssubm  18788  sursubmefmnd  18823  injsubmefmnd  18824  issubgrpd2  19074  grpissubg  19078  subgint  19082  0subgOLD  19084  nmzsubg  19097  eqger  19110  eqgcpbl  19114  cycsubm  19134  cycsubgcl  19138  ghmrn  19161  ghmpreima  19170  gastacl  19241  cntzsubm  19270  sylow2blem1  19550  lsmsubm  19583  torsubg  19784  oddvdssubg  19785  dmdprdd  19931  dprdsubg  19956  dprdres  19960  unitsubm  20295  cntzsubrng  20476  subrgsubm  20494  subrgugrp  20500  subrgint  20504  cntzsubr  20515  issubdrg  20689  lsssubg  20863  islmhm2  20945  pj1lmhm  21007  islbs2  21064  islbs3  21065  lbsextlem4  21071  issubrgd  21096  lidlsubg  21133  2idlcpblrng  21181  isphld  21563  mplsubglem  21908  mplsubrg  21914  mplind  21977  mhpsubg  22040  dmatsgrp  22386  dmatsrng  22388  scmatsgrp  22406  scmatsrng  22407  scmatsgrp1  22409  scmatsrng1  22410  cpmatsubgpmat  22607  cpmatsrgpmat  22608  lmcnp  23191  isufil2  23795  ufileu  23806  filufint  23807  fmfnfm  23845  flimclslem  23871  fclsfnflim  23914  flimfnfcls  23915  fclscmp  23917  clssubg  23996  tgpconncompeqg  23999  tgpconncomp  24000  qustgpopn  24007  tgptsmscls  24037  xmeter  24321  metust  24446  tgqioo  24688  zcld  24702  iccntr  24710  icccmplem2  24712  icccmplem3  24713  reconnlem1  24715  reconnlem2  24716  xrge0tsms  24723  cnheiborlem  24853  om1addcl  24933  pi1blem  24939  pi1grplem  24949  pi1inv  24952  pi1xfr  24955  pi1xfrcnvlem  24956  pi1coghm  24961  cmetcaulem  25188  ivthlem2  25353  ivthlem3  25354  ovolicc2lem2  25419  ovolicc2lem5  25422  opnmbllem  25502  volcn  25507  ismbf3d  25555  mbfi1fseqlem6  25621  itg2const2  25642  i1fibl  25709  ibladd  25722  bddiblnc  25743  ditgsplitlem  25761  dvferm1lem  25888  dvferm2lem  25890  dvlip2  25900  dvivthlem1  25913  dvne0  25916  lhop1lem  25918  lhop1  25919  lhop  25921  dvcnvrelem1  25922  dvcnvrelem2  25923  dvcnvre  25924  ftc1lem1  25942  itgsubst  25956  aaliou3lem2  26251  psercnlem2  26334  efif1olem2  26452  logtayl  26569  log2tlbnd  26855  xrlimcnp  26878  pntibndlem2  27502  pntlemj  27514  pntleml  27522  bday0b  27742  cuteq0  27744  cuteq1  27746  madebdaylemlrcut  27810  cofcut1  27828  onscutlt  28165  trgcgr  28443  hlid  28536  hltr  28537  btwnhl1  28539  btwnhl2  28540  hlcgrex  28543  mirhl  28606  mirbtwnhl  28607  mirhl2  28608  hlpasch  28683  lnopp2hpgb  28690  cgrahl  28754  axlowdim  28888  uhgrissubgr  29202  egrsubgr  29204  uhgrspansubgr  29218  uhgrspan1  29230  cusgrrusgr  29509  wlkonwlk  29590  wlkonwlk1l  29591  wlkres  29598  wlkp1  29609  wlkd  29614  lfgriswlk  29616  wwlksnextinj  29829  2wlkond  29867  wpthswwlks2on  29891  0wlkon  30049  1wlkd  30070  1pthond  30073  eliccelico  32700  elicoelioo  32701  xrge0tsmsd  33002  tpr2rico  33902  measinb  34211  cntmeas  34216  dya2icoseg  34268  sibf0  34325  sibfof  34331  pfxwlk  35111  revwlk  35112  resconn  35233  cvmsss2  35261  cvmliftlem10  35281  mrsubco  35508  cgrextend  35996  cgr3rflx  36042  cgrxfr  36043  btwnconn1lem4  36078  btwnconn1lem8  36082  btwnconn1lem11  36085  bj-pinftynminfty  37215  bj-rveccmod  37290  iooelexlt  37350  opnmbllem0  37650  ibladdnc  37671  ftc1anc  37695  isbnd3  37778  prdsbnd  37787  rngomndo  37929  isgrpda  37949  rngohomco  37968  rngoisocnv  37975  rngoidl  38018  0idl  38019  intidl  38023  unichnidl  38025  keridl  38026  smprngopr  38046  lshpnel2N  38978  lkrshp  39098  4atexlemex2  40065  4atex  40070  cdleme0moN  40219  istendod  40756  dihlspsnat  41327  dochsatshp  41445  mon1psubm  43188  iocinico  43201  dfrtrcl3  43722  eliood  45496  eliccd  45502  eliocd  45505  limciccioolb  45619  limcicciooub  45635  icccncfext  45885  iblspltprt  45971  itgspltprt  45977  fourierdlem1  46106  fourierdlem4  46109  fourierdlem32  46137  fourierdlem33  46138  fourierdlem43  46148  fourierdlem65  46169  fourierdlem79  46183  prsal  46316  issald  46331  iccpartrn  47431  fpprwpprb  47741  bgoldbtbnd  47810  upgrimwlk  47902  upgrimpths  47909  gpgedgvtx0  48052  gpgedgvtx1  48053  gpgprismgr4cycllem11  48095  expnegico01  48507  dignnld  48592  reorelicc  48699