Theorem mpbir3and 1340

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 1126	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
5		mpbir3and.4	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))
6	4, 5	mpbird 257	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  2ellim  8520  canthwelem  10674  intwun  10759  tskwun  10808  gruwun  10837  ixxss1  13375  ixxss2  13376  ixxss12  13377  ixxub  13378  ixxlb  13379  elicod  13407  ubioc1  13410  lbico1  13411  lbicc2  13474  ubicc2  13475  difreicc  13494  supicc  13511  modelico  13879  zmodfz  13891  addmodid  13917  dfrtrcl2  15042  phicl2  16737  4sqlem12  16925  isfuncd  17851  idfucl  17867  cofucl  17874  invfuc  17966  cnvps  18570  psss  18572  issubmd  18758  mndissubm  18759  submid  18762  subsubm  18768  0subm  18769  mhmima  18777  mhmeql  18778  gsumwspan  18798  frmdsssubm  18813  sursubmefmnd  18848  injsubmefmnd  18849  issubgrpd2  19097  grpissubg  19101  subgint  19105  0subgOLD  19107  nmzsubg  19120  eqger  19133  eqgcpbl  19137  cycsubm  19157  cycsubgcl  19161  ghmrn  19183  ghmpreima  19192  gastacl  19260  cntzsubm  19289  sylow2blem1  19575  lsmsubm  19608  torsubg  19809  oddvdssubg  19810  dmdprdd  19956  dprdsubg  19981  dprdres  19985  unitsubm  20325  cntzsubrng  20504  subrgsubm  20524  subrgugrp  20530  subrgint  20534  cntzsubr  20545  issubdrg  20668  lsssubg  20841  islmhm2  20923  pj1lmhm  20985  islbs2  21042  islbs3  21043  lbsextlem4  21049  issubrgd  21082  lidlsubg  21119  2idlcpblrng  21165  isphld  21586  mplsubglem  21941  mplsubrg  21947  mplind  22014  mhpsubg  22077  dmatsgrp  22414  dmatsrng  22416  scmatsgrp  22434  scmatsrng  22435  scmatsgrp1  22437  scmatsrng1  22438  cpmatsubgpmat  22635  cpmatsrgpmat  22636  lmcnp  23221  isufil2  23825  ufileu  23836  filufint  23837  fmfnfm  23875  flimclslem  23901  fclsfnflim  23944  flimfnfcls  23945  fclscmp  23947  clssubg  24026  tgpconncompeqg  24029  tgpconncomp  24030  qustgpopn  24037  tgptsmscls  24067  xmeter  24352  metust  24480  tgqioo  24729  zcld  24742  iccntr  24750  icccmplem2  24752  icccmplem3  24753  reconnlem1  24755  reconnlem2  24756  xrge0tsms  24763  cnheiborlem  24893  om1addcl  24973  pi1blem  24979  pi1grplem  24989  pi1inv  24992  pi1xfr  24995  pi1xfrcnvlem  24996  pi1coghm  25001  cmetcaulem  25229  ivthlem2  25394  ivthlem3  25395  ovolicc2lem2  25460  ovolicc2lem5  25463  opnmbllem  25543  volcn  25548  ismbf3d  25596  mbfi1fseqlem6  25663  itg2const2  25684  i1fibl  25750  ibladd  25763  bddiblnc  25784  ditgsplitlem  25802  dvferm1lem  25929  dvferm2lem  25931  dvlip2  25941  dvivthlem1  25954  dvne0  25957  lhop1lem  25959  lhop1  25960  lhop  25962  dvcnvrelem1  25963  dvcnvrelem2  25964  dvcnvre  25965  ftc1lem1  25983  itgsubst  25997  aaliou3lem2  26291  psercnlem2  26374  efif1olem2  26490  logtayl  26607  log2tlbnd  26890  xrlimcnp  26913  pntibndlem2  27537  pntlemj  27549  pntleml  27557  bday0b  27776  cuteq0  27778  cuteq1  27779  madebdaylemlrcut  27838  cofcut1  27853  trgcgr  28333  hlid  28426  hltr  28427  btwnhl1  28429  btwnhl2  28430  hlcgrex  28433  mirhl  28496  mirbtwnhl  28497  mirhl2  28498  hlpasch  28573  lnopp2hpgb  28580  cgrahl  28644  axlowdim  28785  uhgrissubgr  29101  egrsubgr  29103  uhgrspansubgr  29117  uhgrspan1  29129  cusgrrusgr  29408  wlkonwlk  29489  wlkonwlk1l  29490  wlkres  29497  wlkp1  29508  wlkd  29513  lfgriswlk  29515  wwlksnextinj  29723  2wlkond  29761  wpthswwlks2on  29785  0wlkon  29943  1wlkd  29964  1pthond  29967  eliccelico  32558  elicoelioo  32559  xrge0tsmsd  32784  tpr2rico  33513  measinb  33840  cntmeas  33845  dya2icoseg  33897  sibf0  33954  sibfof  33960  pfxwlk  34733  revwlk  34734  resconn  34856  cvmsss2  34884  cvmliftlem10  34904  mrsubco  35131  cgrextend  35604  cgr3rflx  35650  cgrxfr  35651  btwnconn1lem4  35686  btwnconn1lem8  35690  btwnconn1lem11  35693  bj-pinftynminfty  36706  bj-rveccmod  36781  iooelexlt  36841  opnmbllem0  37129  ibladdnc  37150  ftc1anc  37174  isbnd3  37257  prdsbnd  37266  rngomndo  37408  isgrpda  37428  rngohomco  37447  rngoisocnv  37454  rngoidl  37497  0idl  37498  intidl  37502  unichnidl  37504  keridl  37505  smprngopr  37525  lshpnel2N  38457  lkrshp  38577  4atexlemex2  39544  4atex  39549  cdleme0moN  39698  istendod  40235  dihlspsnat  40806  dochsatshp  40924  mon1psubm  42627  iocinico  42640  dfrtrcl3  43163  eliood  44883  eliccd  44889  eliocd  44892  limciccioolb  45009  limcicciooub  45025  icccncfext  45275  iblspltprt  45361  itgspltprt  45367  fourierdlem1  45496  fourierdlem4  45499  fourierdlem32  45527  fourierdlem33  45528  fourierdlem43  45538  fourierdlem65  45559  fourierdlem79  45573  prsal  45706  issald  45721  iccpartrn  46770  fpprwpprb  47080  bgoldbtbnd  47149  expnegico01  47586  dignnld  47676  reorelicc  47783