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

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

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 398  df-3an 1090

This theorem is referenced by:  2ellim  8499  canthwelem  10645  intwun  10730  tskwun  10779  gruwun  10808  ixxss1  13342  ixxss2  13343  ixxss12  13344  ixxub  13345  ixxlb  13346  elicod  13374  ubioc1  13377  lbico1  13378  lbicc2  13441  ubicc2  13442  difreicc  13461  supicc  13478  modelico  13846  zmodfz  13858  addmodid  13884  dfrtrcl2  15009  phicl2  16701  4sqlem12  16889  isfuncd  17815  idfucl  17831  cofucl  17838  invfuc  17927  cnvps  18531  psss  18533  issubmd  18687  mndissubm  18688  submid  18691  subsubm  18697  0subm  18698  mhmima  18706  mhmeql  18707  gsumwspan  18727  frmdsssubm  18742  sursubmefmnd  18777  injsubmefmnd  18778  issubgrpd2  19022  grpissubg  19026  subgint  19030  0subgOLD  19032  nmzsubg  19045  eqger  19058  eqgcpbl  19062  cycsubm  19079  cycsubgcl  19083  ghmrn  19105  ghmpreima  19114  gastacl  19173  cntzsubm  19202  sylow2blem1  19488  lsmsubm  19521  torsubg  19722  oddvdssubg  19723  dmdprdd  19869  dprdsubg  19894  dprdres  19898  unitsubm  20200  subrgsubm  20332  subrgugrp  20338  subrgint  20342  cntzsubr  20353  issubdrg  20401  lsssubg  20568  islmhm2  20649  pj1lmhm  20711  islbs2  20767  islbs3  20768  lbsextlem4  20774  issubrgd  20811  lidlsubg  20838  2idlcpbl  20871  isphld  21207  mplsubglem  21558  mplsubrg  21564  mplind  21631  mhpsubg  21696  dmatsgrp  22001  dmatsrng  22003  scmatsgrp  22021  scmatsrng  22022  scmatsgrp1  22024  scmatsrng1  22025  cpmatsubgpmat  22222  cpmatsrgpmat  22223  lmcnp  22808  isufil2  23412  ufileu  23423  filufint  23424  fmfnfm  23462  flimclslem  23488  fclsfnflim  23531  flimfnfcls  23532  fclscmp  23534  clssubg  23613  tgpconncompeqg  23616  tgpconncomp  23617  qustgpopn  23624  tgptsmscls  23654  xmeter  23939  metust  24067  tgqioo  24316  zcld  24329  iccntr  24337  icccmplem2  24339  icccmplem3  24340  reconnlem1  24342  reconnlem2  24343  xrge0tsms  24350  cnheiborlem  24470  om1addcl  24549  pi1blem  24555  pi1grplem  24565  pi1inv  24568  pi1xfr  24571  pi1xfrcnvlem  24572  pi1coghm  24577  cmetcaulem  24805  ivthlem2  24969  ivthlem3  24970  ovolicc2lem2  25035  ovolicc2lem5  25038  opnmbllem  25118  volcn  25123  ismbf3d  25171  mbfi1fseqlem6  25238  itg2const2  25259  i1fibl  25325  ibladd  25338  bddiblnc  25359  ditgsplitlem  25377  dvferm1lem  25501  dvferm2lem  25503  dvlip2  25512  dvivthlem1  25525  dvne0  25528  lhop1lem  25530  lhop1  25531  lhop  25533  dvcnvrelem1  25534  dvcnvrelem2  25535  dvcnvre  25536  ftc1lem1  25552  itgsubst  25566  aaliou3lem2  25856  psercnlem2  25936  efif1olem2  26052  logtayl  26168  log2tlbnd  26450  xrlimcnp  26473  pntibndlem2  27094  pntlemj  27106  pntleml  27114  bday0b  27331  cuteq0  27333  cuteq1  27334  madebdaylemlrcut  27393  cofcut1  27407  trgcgr  27767  hlid  27860  hltr  27861  btwnhl1  27863  btwnhl2  27864  hlcgrex  27867  mirhl  27930  mirbtwnhl  27931  mirhl2  27932  hlpasch  28007  lnopp2hpgb  28014  cgrahl  28078  axlowdim  28219  uhgrissubgr  28532  egrsubgr  28534  uhgrspansubgr  28548  uhgrspan1  28560  cusgrrusgr  28838  wlkonwlk  28919  wlkonwlk1l  28920  wlkres  28927  wlkp1  28938  wlkd  28943  lfgriswlk  28945  wwlksnextinj  29153  2wlkond  29191  wpthswwlks2on  29215  0wlkon  29373  1wlkd  29394  1pthond  29397  eliccelico  31988  elicoelioo  31989  xrge0tsmsd  32209  tpr2rico  32892  measinb  33219  cntmeas  33224  dya2icoseg  33276  sibf0  33333  sibfof  33339  pfxwlk  34114  revwlk  34115  resconn  34237  cvmsss2  34265  cvmliftlem10  34285  mrsubco  34512  cgrextend  34980  cgr3rflx  35026  cgrxfr  35027  btwnconn1lem4  35062  btwnconn1lem8  35066  btwnconn1lem11  35069  bj-pinftynminfty  36108  bj-rveccmod  36183  iooelexlt  36243  opnmbllem0  36524  ibladdnc  36545  ftc1anc  36569  isbnd3  36652  prdsbnd  36661  rngomndo  36803  isgrpda  36823  rngohomco  36842  rngoisocnv  36849  rngoidl  36892  0idl  36893  intidl  36897  unichnidl  36899  keridl  36900  smprngopr  36920  lshpnel2N  37855  lkrshp  37975  4atexlemex2  38942  4atex  38947  cdleme0moN  39096  istendod  39633  dihlspsnat  40204  dochsatshp  40322  mon1psubm  41948  iocinico  41961  dfrtrcl3  42484  eliood  44211  eliccd  44217  eliocd  44220  limciccioolb  44337  limcicciooub  44353  icccncfext  44603  iblspltprt  44689  itgspltprt  44695  fourierdlem1  44824  fourierdlem4  44827  fourierdlem32  44855  fourierdlem33  44856  fourierdlem43  44866  fourierdlem65  44887  fourierdlem79  44901  prsal  45034  issald  45049  iccpartrn  46098  fpprwpprb  46408  bgoldbtbnd  46477  cntzsubrng  46746  2idlcpblrng  46766  expnegico01  47199  dignnld  47289  reorelicc  47396