Theorem mpbir3and 1361

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  2ellim  8489  canthwelem  10662  intwun  10747  tskwun  10796  gruwun  10825  ixxss1  13418  ixxss2  13419  ixxss12  13420  ixxub  13421  ixxlb  13422  elicod  13450  ubioc1  13454  lbico1  13455  lbicc2  13519  ubicc2  13520  difreicc  13539  supicc  13556  nnge2recico01  13562  modelico  13944  zmodfz  13956  addmodid  13985  dfrtrcl2  15137  phicl2  16863  4sqlem12  17052  isfuncd  17958  idfucl  17974  cofucl  17981  invfuc  18070  cnvps  18670  psss  18672  issubmd  18915  mndissubm  18916  submid  18919  subsubm  18926  0subm  18927  mhmima  18935  mhmeql  18936  gsumwspan  18956  frmdsssubm  18971  sursubmefmnd  19006  injsubmefmnd  19007  issubgrpd2  19267  grpissubg  19271  subgint  19275  nmzsubg  19289  eqger  19304  eqgcpbl  19308  cycsubm  19331  cycsubgcl  19335  ghmrn  19357  ghmpreima  19366  gastacl  19437  cntzsubm  19466  sylow2blem1  19748  lsmsubm  19781  torsubg  19982  oddvdssubg  19983  dmdprdd  20129  dprdsubg  20154  dprdres  20158  unitsubm  20528  cntzsubrng  20730  subrgsubm  20748  subrgugrp  20754  subrgint  20758  cntzsubr  20769  issubdrg  20947  lsssubg  21142  islmhm2  21223  pj1lmhm  21285  islbs2  21342  islbs3  21343  lbsextlem4  21349  issubrgd  21374  lidlsubg  21412  2idlcpblrng  21474  isphld  21868  mplsubglem  22214  mplsubrg  22220  mplind  22287  mhpsubg  22382  dmatsgrp  22722  dmatsrng  22724  scmatsgrp  22742  scmatsrng  22743  scmatsgrp1  22745  scmatsrng1  22746  cpmatsubgpmat  22946  cpmatsrgpmat  22947  lmcnp  23530  isufil2  24135  ufileu  24146  filufint  24147  fmfnfm  24185  flimclslem  24211  fclsfnflim  24254  flimfnfcls  24255  fclscmp  24257  clssubg  24336  tgpconncompeqg  24339  tgpconncomp  24340  qustgpopn  24347  tgptsmscls  24377  xmeter  24660  metust  24785  tgqioo  25027  zcld  25041  iccntr  25049  icccmplem2  25051  icccmplem3  25052  reconnlem1  25054  reconnlem2  25055  xrge0tsms  25062  cnheiborlem  25183  om1addcl  25262  pi1blem  25268  pi1grplem  25278  pi1inv  25281  pi1xfr  25284  pi1xfrcnvlem  25285  pi1coghm  25290  cmetcaulem  25517  ivthlem2  25681  ivthlem3  25682  ovolicc2lem2  25747  ovolicc2lem5  25750  opnmbllem  25830  volcn  25835  ismbf3d  25883  mbfi1fseqlem6  25949  itg2const2  25970  i1fibl  26037  ibladd  26050  bddiblnc  26071  ditgsplitlem  26089  dvferm1lem  26213  dvferm2lem  26215  dvlip2  26224  dvivthlem1  26237  dvne0  26240  lhop1lem  26242  lhop1  26243  lhop  26245  dvcnvrelem1  26246  dvcnvrelem2  26247  dvcnvre  26248  ftc1lem1  26264  itgsubst  26278  aaliou3lem2  26576  psercnlem2  26657  efif1olem2  26778  logtayl  26895  log2tlbnd  27180  xrlimcnp  27203  pntibndlem2  27825  pntlemj  27837  pntleml  27845  bday0b  28076  cuteq0  28078  cuteq1  28080  madebdaylemlrcut  28162  cofcut1  28183  oncutlt  28527  trgcgr  28856  hlid  28952  hltr  28953  btwnhl1  28955  btwnhl2  28956  hlcgrex  28959  mirhl  29028  mirbtwnhl  29029  mirhl2  29030  hlpasch  29111  lnopp2hpgb  29118  cgrahl  29212  axlowdim  29404  uhgrissubgr  29721  egrsubgr  29723  uhgrspansubgr  29737  uhgrspan1  29749  cusgrrusgr  30027  wlkonwlk  30106  wlkonwlk1l  30107  wlkres  30114  wlkp1  30125  wlkd  30130  pfxwlk  30131  revwlk  30132  lfgriswlk  30136  wwlksnextinj  30353  2wlkond  30391  wpthswwlks2on  30418  0wlkon  30576  1wlkd  30597  1pthond  30600  eliccelico  33235  elicoelioo  33236  xrge0tsmsd  33500  tpr2rico  34409  measinb  34719  cntmeas  34724  dya2icoseg  34775  sibf0  34832  sibfof  34838  resconn  35812  cvmsss2  35840  cvmliftlem10  35860  mrsubco  36087  cgrextend  36575  cgr3rflx  36621  cgrxfr  36622  btwnconn1lem4  36657  btwnconn1lem8  36661  btwnconn1lem11  36664  bj-pinftynminfty  37966  bj-rveccmod  38041  iooelexlt  38103  opnmbllem0  38392  ibladdnc  38413  ftc1anc  38437  isbnd3  38521  prdsbnd  38530  rngomndo  38672  isgrpda  38692  rngohomco  38711  rngoisocnv  38718  rngoidl  38761  0idl  38762  intidl  38766  unichnidl  38768  keridl  38769  smprngopr  38789  lshpnel2N  39845  lkrshp  39965  4atexlemex2  40931  4atex  40936  cdleme0moN  41085  istendod  41622  dihlspsnat  42193  dochsatshp  42311  mon1psubm  44027  iocinico  44040  dfrtrcl3  44560  eliood  46315  eliccd  46321  eliocd  46324  limciccioolb  46438  limcicciooub  46452  icccncfext  46702  iblspltprt  46788  itgspltprt  46794  fourierdlem1  46923  fourierdlem4  46926  fourierdlem32  46954  fourierdlem33  46955  fourierdlem43  46965  fourierdlem65  46986  fourierdlem79  47000  prsal  47133  issald  47148  flmrecm1  48218  iccpartrn  48317  fpprwpprb  48643  bgoldbtbnd  48712  upgrimwlk  48805  upgrimpths  48812  gpgedgvtx0  48964  gpgedgvtx1  48965  gpgprismgr4cycllem11  49008  smprngprmrng  49241  expnegico01  49435  dignnld  49520  reorelicc  49627