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  8409  canthwelem  10533  intwun  10618  tskwun  10667  gruwun  10696  ixxss1  13255  ixxss2  13256  ixxss12  13257  ixxub  13258  ixxlb  13259  elicod  13287  ubioc1  13291  lbico1  13292  lbicc2  13356  ubicc2  13357  difreicc  13376  supicc  13393  modelico  13777  zmodfz  13789  addmodid  13818  dfrtrcl2  14961  phicl2  16671  4sqlem12  16860  isfuncd  17764  idfucl  17780  cofucl  17787  invfuc  17876  cnvps  18476  psss  18478  issubmd  18706  mndissubm  18707  submid  18710  subsubm  18716  0subm  18717  mhmima  18725  mhmeql  18726  gsumwspan  18746  frmdsssubm  18761  sursubmefmnd  18796  injsubmefmnd  18797  issubgrpd2  19047  grpissubg  19051  subgint  19055  0subgOLD  19057  nmzsubg  19070  eqger  19083  eqgcpbl  19087  cycsubm  19107  cycsubgcl  19111  ghmrn  19134  ghmpreima  19143  gastacl  19214  cntzsubm  19243  sylow2blem1  19525  lsmsubm  19558  torsubg  19759  oddvdssubg  19760  dmdprdd  19906  dprdsubg  19931  dprdres  19935  unitsubm  20297  cntzsubrng  20475  subrgsubm  20493  subrgugrp  20499  subrgint  20503  cntzsubr  20514  issubdrg  20688  lsssubg  20883  islmhm2  20965  pj1lmhm  21027  islbs2  21084  islbs3  21085  lbsextlem4  21091  issubrgd  21116  lidlsubg  21153  2idlcpblrng  21201  isphld  21584  mplsubglem  21929  mplsubrg  21935  mplind  21998  mhpsubg  22061  dmatsgrp  22407  dmatsrng  22409  scmatsgrp  22427  scmatsrng  22428  scmatsgrp1  22430  scmatsrng1  22431  cpmatsubgpmat  22628  cpmatsrgpmat  22629  lmcnp  23212  isufil2  23816  ufileu  23827  filufint  23828  fmfnfm  23866  flimclslem  23892  fclsfnflim  23935  flimfnfcls  23936  fclscmp  23938  clssubg  24017  tgpconncompeqg  24020  tgpconncomp  24021  qustgpopn  24028  tgptsmscls  24058  xmeter  24341  metust  24466  tgqioo  24708  zcld  24722  iccntr  24730  icccmplem2  24732  icccmplem3  24733  reconnlem1  24735  reconnlem2  24736  xrge0tsms  24743  cnheiborlem  24873  om1addcl  24953  pi1blem  24959  pi1grplem  24969  pi1inv  24972  pi1xfr  24975  pi1xfrcnvlem  24976  pi1coghm  24981  cmetcaulem  25208  ivthlem2  25373  ivthlem3  25374  ovolicc2lem2  25439  ovolicc2lem5  25442  opnmbllem  25522  volcn  25527  ismbf3d  25575  mbfi1fseqlem6  25641  itg2const2  25662  i1fibl  25729  ibladd  25742  bddiblnc  25763  ditgsplitlem  25781  dvferm1lem  25908  dvferm2lem  25910  dvlip2  25920  dvivthlem1  25933  dvne0  25936  lhop1lem  25938  lhop1  25939  lhop  25941  dvcnvrelem1  25942  dvcnvrelem2  25943  dvcnvre  25944  ftc1lem1  25962  itgsubst  25976  aaliou3lem2  26271  psercnlem2  26354  efif1olem2  26472  logtayl  26589  log2tlbnd  26875  xrlimcnp  26898  pntibndlem2  27522  pntlemj  27534  pntleml  27542  bday0b  27767  cuteq0  27769  cuteq1  27771  madebdaylemlrcut  27837  cofcut1  27857  onscutlt  28194  trgcgr  28487  hlid  28580  hltr  28581  btwnhl1  28583  btwnhl2  28584  hlcgrex  28587  mirhl  28650  mirbtwnhl  28651  mirhl2  28652  hlpasch  28727  lnopp2hpgb  28734  cgrahl  28798  axlowdim  28932  uhgrissubgr  29246  egrsubgr  29248  uhgrspansubgr  29262  uhgrspan1  29274  cusgrrusgr  29553  wlkonwlk  29632  wlkonwlk1l  29633  wlkres  29640  wlkp1  29651  wlkd  29656  lfgriswlk  29658  wwlksnextinj  29870  2wlkond  29908  wpthswwlks2on  29932  0wlkon  30090  1wlkd  30111  1pthond  30114  eliccelico  32750  elicoelioo  32751  xrge0tsmsd  33032  tpr2rico  33915  measinb  34224  cntmeas  34229  dya2icoseg  34280  sibf0  34337  sibfof  34343  pfxwlk  35136  revwlk  35137  resconn  35258  cvmsss2  35286  cvmliftlem10  35306  mrsubco  35533  cgrextend  36021  cgr3rflx  36067  cgrxfr  36068  btwnconn1lem4  36103  btwnconn1lem8  36107  btwnconn1lem11  36110  bj-pinftynminfty  37240  bj-rveccmod  37315  iooelexlt  37375  opnmbllem0  37675  ibladdnc  37696  ftc1anc  37720  isbnd3  37803  prdsbnd  37812  rngomndo  37954  isgrpda  37974  rngohomco  37993  rngoisocnv  38000  rngoidl  38043  0idl  38044  intidl  38048  unichnidl  38050  keridl  38051  smprngopr  38071  lshpnel2N  39003  lkrshp  39123  4atexlemex2  40089  4atex  40094  cdleme0moN  40243  istendod  40780  dihlspsnat  41351  dochsatshp  41469  mon1psubm  43211  iocinico  43224  dfrtrcl3  43745  eliood  45517  eliccd  45523  eliocd  45526  limciccioolb  45640  limcicciooub  45654  icccncfext  45904  iblspltprt  45990  itgspltprt  45996  fourierdlem1  46125  fourierdlem4  46128  fourierdlem32  46156  fourierdlem33  46157  fourierdlem43  46167  fourierdlem65  46188  fourierdlem79  46202  prsal  46335  issald  46350  iccpartrn  47440  fpprwpprb  47750  bgoldbtbnd  47819  upgrimwlk  47912  upgrimpths  47919  gpgedgvtx0  48071  gpgedgvtx1  48072  gpgprismgr4cycllem11  48115  expnegico01  48529  dignnld  48614  reorelicc  48721