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

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

This theorem is referenced by:  2ellim  8555  canthwelem  10719  intwun  10804  tskwun  10853  gruwun  10882  ixxss1  13425  ixxss2  13426  ixxss12  13427  ixxub  13428  ixxlb  13429  elicod  13457  ubioc1  13460  lbico1  13461  lbicc2  13524  ubicc2  13525  difreicc  13544  supicc  13561  modelico  13932  zmodfz  13944  addmodid  13970  dfrtrcl2  15111  phicl2  16815  4sqlem12  17003  isfuncd  17929  idfucl  17945  cofucl  17952  invfuc  18044  cnvps  18648  psss  18650  issubmd  18841  mndissubm  18842  submid  18845  subsubm  18851  0subm  18852  mhmima  18860  mhmeql  18861  gsumwspan  18881  frmdsssubm  18896  sursubmefmnd  18931  injsubmefmnd  18932  issubgrpd2  19182  grpissubg  19186  subgint  19190  0subgOLD  19192  nmzsubg  19205  eqger  19218  eqgcpbl  19222  cycsubm  19242  cycsubgcl  19246  ghmrn  19269  ghmpreima  19278  gastacl  19349  cntzsubm  19378  sylow2blem1  19662  lsmsubm  19695  torsubg  19896  oddvdssubg  19897  dmdprdd  20043  dprdsubg  20068  dprdres  20072  unitsubm  20412  cntzsubrng  20593  subrgsubm  20613  subrgugrp  20619  subrgint  20623  cntzsubr  20634  issubdrg  20803  lsssubg  20978  islmhm2  21060  pj1lmhm  21122  islbs2  21179  islbs3  21180  lbsextlem4  21186  issubrgd  21219  lidlsubg  21256  2idlcpblrng  21304  isphld  21695  mplsubglem  22042  mplsubrg  22048  mplind  22117  mhpsubg  22180  dmatsgrp  22526  dmatsrng  22528  scmatsgrp  22546  scmatsrng  22547  scmatsgrp1  22549  scmatsrng1  22550  cpmatsubgpmat  22747  cpmatsrgpmat  22748  lmcnp  23333  isufil2  23937  ufileu  23948  filufint  23949  fmfnfm  23987  flimclslem  24013  fclsfnflim  24056  flimfnfcls  24057  fclscmp  24059  clssubg  24138  tgpconncompeqg  24141  tgpconncomp  24142  qustgpopn  24149  tgptsmscls  24179  xmeter  24464  metust  24592  tgqioo  24841  zcld  24854  iccntr  24862  icccmplem2  24864  icccmplem3  24865  reconnlem1  24867  reconnlem2  24868  xrge0tsms  24875  cnheiborlem  25005  om1addcl  25085  pi1blem  25091  pi1grplem  25101  pi1inv  25104  pi1xfr  25107  pi1xfrcnvlem  25108  pi1coghm  25113  cmetcaulem  25341  ivthlem2  25506  ivthlem3  25507  ovolicc2lem2  25572  ovolicc2lem5  25575  opnmbllem  25655  volcn  25660  ismbf3d  25708  mbfi1fseqlem6  25775  itg2const2  25796  i1fibl  25863  ibladd  25876  bddiblnc  25897  ditgsplitlem  25915  dvferm1lem  26042  dvferm2lem  26044  dvlip2  26054  dvivthlem1  26067  dvne0  26070  lhop1lem  26072  lhop1  26073  lhop  26075  dvcnvrelem1  26076  dvcnvrelem2  26077  dvcnvre  26078  ftc1lem1  26096  itgsubst  26110  aaliou3lem2  26403  psercnlem2  26486  efif1olem2  26603  logtayl  26720  log2tlbnd  27006  xrlimcnp  27029  pntibndlem2  27653  pntlemj  27665  pntleml  27673  bday0b  27893  cuteq0  27895  cuteq1  27896  madebdaylemlrcut  27955  cofcut1  27972  trgcgr  28542  hlid  28635  hltr  28636  btwnhl1  28638  btwnhl2  28639  hlcgrex  28642  mirhl  28705  mirbtwnhl  28706  mirhl2  28707  hlpasch  28782  lnopp2hpgb  28789  cgrahl  28853  axlowdim  28994  uhgrissubgr  29310  egrsubgr  29312  uhgrspansubgr  29326  uhgrspan1  29338  cusgrrusgr  29617  wlkonwlk  29698  wlkonwlk1l  29699  wlkres  29706  wlkp1  29717  wlkd  29722  lfgriswlk  29724  wwlksnextinj  29932  2wlkond  29970  wpthswwlks2on  29994  0wlkon  30152  1wlkd  30173  1pthond  30176  eliccelico  32782  elicoelioo  32783  xrge0tsmsd  33041  tpr2rico  33858  measinb  34185  cntmeas  34190  dya2icoseg  34242  sibf0  34299  sibfof  34305  pfxwlk  35091  revwlk  35092  resconn  35214  cvmsss2  35242  cvmliftlem10  35262  mrsubco  35489  cgrextend  35972  cgr3rflx  36018  cgrxfr  36019  btwnconn1lem4  36054  btwnconn1lem8  36058  btwnconn1lem11  36061  bj-pinftynminfty  37193  bj-rveccmod  37268  iooelexlt  37328  opnmbllem0  37616  ibladdnc  37637  ftc1anc  37661  isbnd3  37744  prdsbnd  37753  rngomndo  37895  isgrpda  37915  rngohomco  37934  rngoisocnv  37941  rngoidl  37984  0idl  37985  intidl  37989  unichnidl  37991  keridl  37992  smprngopr  38012  lshpnel2N  38941  lkrshp  39061  4atexlemex2  40028  4atex  40033  cdleme0moN  40182  istendod  40719  dihlspsnat  41290  dochsatshp  41408  mon1psubm  43160  iocinico  43173  dfrtrcl3  43695  eliood  45416  eliccd  45422  eliocd  45425  limciccioolb  45542  limcicciooub  45558  icccncfext  45808  iblspltprt  45894  itgspltprt  45900  fourierdlem1  46029  fourierdlem4  46032  fourierdlem32  46060  fourierdlem33  46061  fourierdlem43  46071  fourierdlem65  46092  fourierdlem79  46106  prsal  46239  issald  46254  iccpartrn  47304  fpprwpprb  47614  bgoldbtbnd  47683  expnegico01  48247  dignnld  48337  reorelicc  48444