Theorem mpbir3and 1341

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 1127	. 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  8535  canthwelem  10687  intwun  10772  tskwun  10821  gruwun  10850  ixxss1  13401  ixxss2  13402  ixxss12  13403  ixxub  13404  ixxlb  13405  elicod  13433  ubioc1  13436  lbico1  13437  lbicc2  13500  ubicc2  13501  difreicc  13520  supicc  13537  modelico  13917  zmodfz  13929  addmodid  13956  dfrtrcl2  15097  phicl2  16801  4sqlem12  16989  isfuncd  17915  idfucl  17931  cofucl  17938  invfuc  18030  cnvps  18635  psss  18637  issubmd  18831  mndissubm  18832  submid  18835  subsubm  18841  0subm  18842  mhmima  18850  mhmeql  18851  gsumwspan  18871  frmdsssubm  18886  sursubmefmnd  18921  injsubmefmnd  18922  issubgrpd2  19172  grpissubg  19176  subgint  19180  0subgOLD  19182  nmzsubg  19195  eqger  19208  eqgcpbl  19212  cycsubm  19232  cycsubgcl  19236  ghmrn  19259  ghmpreima  19268  gastacl  19339  cntzsubm  19368  sylow2blem1  19652  lsmsubm  19685  torsubg  19886  oddvdssubg  19887  dmdprdd  20033  dprdsubg  20058  dprdres  20062  unitsubm  20402  cntzsubrng  20583  subrgsubm  20601  subrgugrp  20607  subrgint  20611  cntzsubr  20622  issubdrg  20797  lsssubg  20972  islmhm2  21054  pj1lmhm  21116  islbs2  21173  islbs3  21174  lbsextlem4  21180  issubrgd  21213  lidlsubg  21250  2idlcpblrng  21298  isphld  21689  mplsubglem  22036  mplsubrg  22042  mplind  22111  mhpsubg  22174  dmatsgrp  22520  dmatsrng  22522  scmatsgrp  22540  scmatsrng  22541  scmatsgrp1  22543  scmatsrng1  22544  cpmatsubgpmat  22741  cpmatsrgpmat  22742  lmcnp  23327  isufil2  23931  ufileu  23942  filufint  23943  fmfnfm  23981  flimclslem  24007  fclsfnflim  24050  flimfnfcls  24051  fclscmp  24053  clssubg  24132  tgpconncompeqg  24135  tgpconncomp  24136  qustgpopn  24143  tgptsmscls  24173  xmeter  24458  metust  24586  tgqioo  24835  zcld  24848  iccntr  24856  icccmplem2  24858  icccmplem3  24859  reconnlem1  24861  reconnlem2  24862  xrge0tsms  24869  cnheiborlem  24999  om1addcl  25079  pi1blem  25085  pi1grplem  25095  pi1inv  25098  pi1xfr  25101  pi1xfrcnvlem  25102  pi1coghm  25107  cmetcaulem  25335  ivthlem2  25500  ivthlem3  25501  ovolicc2lem2  25566  ovolicc2lem5  25569  opnmbllem  25649  volcn  25654  ismbf3d  25702  mbfi1fseqlem6  25769  itg2const2  25790  i1fibl  25857  ibladd  25870  bddiblnc  25891  ditgsplitlem  25909  dvferm1lem  26036  dvferm2lem  26038  dvlip2  26048  dvivthlem1  26061  dvne0  26064  lhop1lem  26066  lhop1  26067  lhop  26069  dvcnvrelem1  26070  dvcnvrelem2  26071  dvcnvre  26072  ftc1lem1  26090  itgsubst  26104  aaliou3lem2  26399  psercnlem2  26482  efif1olem2  26599  logtayl  26716  log2tlbnd  27002  xrlimcnp  27025  pntibndlem2  27649  pntlemj  27661  pntleml  27669  bday0b  27889  cuteq0  27891  cuteq1  27892  madebdaylemlrcut  27951  cofcut1  27968  trgcgr  28538  hlid  28631  hltr  28632  btwnhl1  28634  btwnhl2  28635  hlcgrex  28638  mirhl  28701  mirbtwnhl  28702  mirhl2  28703  hlpasch  28778  lnopp2hpgb  28785  cgrahl  28849  axlowdim  28990  uhgrissubgr  29306  egrsubgr  29308  uhgrspansubgr  29322  uhgrspan1  29334  cusgrrusgr  29613  wlkonwlk  29694  wlkonwlk1l  29695  wlkres  29702  wlkp1  29713  wlkd  29718  lfgriswlk  29720  wwlksnextinj  29928  2wlkond  29966  wpthswwlks2on  29990  0wlkon  30148  1wlkd  30169  1pthond  30172  eliccelico  32785  elicoelioo  32786  xrge0tsmsd  33047  tpr2rico  33872  measinb  34201  cntmeas  34206  dya2icoseg  34258  sibf0  34315  sibfof  34321  pfxwlk  35107  revwlk  35108  resconn  35230  cvmsss2  35258  cvmliftlem10  35278  mrsubco  35505  cgrextend  35989  cgr3rflx  36035  cgrxfr  36036  btwnconn1lem4  36071  btwnconn1lem8  36075  btwnconn1lem11  36078  bj-pinftynminfty  37209  bj-rveccmod  37284  iooelexlt  37344  opnmbllem0  37642  ibladdnc  37663  ftc1anc  37687  isbnd3  37770  prdsbnd  37779  rngomndo  37921  isgrpda  37941  rngohomco  37960  rngoisocnv  37967  rngoidl  38010  0idl  38011  intidl  38015  unichnidl  38017  keridl  38018  smprngopr  38038  lshpnel2N  38966  lkrshp  39086  4atexlemex2  40053  4atex  40058  cdleme0moN  40207  istendod  40744  dihlspsnat  41315  dochsatshp  41433  mon1psubm  43187  iocinico  43200  dfrtrcl3  43722  eliood  45450  eliccd  45456  eliocd  45459  limciccioolb  45576  limcicciooub  45592  icccncfext  45842  iblspltprt  45928  itgspltprt  45934  fourierdlem1  46063  fourierdlem4  46066  fourierdlem32  46094  fourierdlem33  46095  fourierdlem43  46105  fourierdlem65  46126  fourierdlem79  46140  prsal  46273  issald  46288  iccpartrn  47354  fpprwpprb  47664  bgoldbtbnd  47733  gpgedgvtx0  47953  gpgedgvtx1  47954  expnegico01  48363  dignnld  48452  reorelicc  48559