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  8507  canthwelem  10735  intwun  10820  tskwun  10869  gruwun  10898  ixxss1  13494  ixxss2  13495  ixxss12  13496  ixxub  13497  ixxlb  13498  elicod  13526  ubioc1  13530  lbico1  13531  lbicc2  13595  ubicc2  13596  difreicc  13615  supicc  13632  nnge2recico01  13638  modelico  14021  zmodfz  14033  addmodid  14062  dfrtrcl2  15215  phicl2  16945  4sqlem12  17134  isfuncd  18040  idfucl  18056  cofucl  18063  invfuc  18152  cnvps  18752  psss  18754  issubmd  19001  mndissubm  19002  submid  19005  subsubm  19012  0subm  19013  mhmima  19021  mhmeql  19022  gsumwspan  19042  frmdsssubm  19057  sursubmefmnd  19092  injsubmefmnd  19093  issubgrpd2  19353  grpissubg  19357  subgint  19361  nmzsubg  19375  eqger  19390  eqgcpbl  19394  cycsubm  19417  cycsubgcl  19421  ghmrn  19443  ghmpreima  19452  gastacl  19523  cntzsubm  19552  sylow2blem1  19834  lsmsubm  19867  torsubg  20068  oddvdssubg  20069  dmdprdd  20215  dprdsubg  20240  dprdres  20244  unitsubm  20616  cntzsubrng  20819  subrgsubm  20837  subrgugrp  20843  subrgint  20847  cntzsubr  20858  issubdrg  21037  lsssubg  21232  islmhm2  21313  pj1lmhm  21375  islbs2  21432  islbs3  21433  lbsextlem4  21439  issubrgd  21464  lidlsubg  21502  2idlcpblrng  21565  isphld  21960  mplsubglem  22306  mplsubrg  22312  mplind  22379  mhpsubg  22474  dmatsgrp  22814  dmatsrng  22816  scmatsgrp  22834  scmatsrng  22835  scmatsgrp1  22837  scmatsrng1  22838  cpmatsubgpmat  23038  cpmatsrgpmat  23039  lmcnp  23622  isufil2  24227  ufileu  24238  filufint  24239  fmfnfm  24277  flimclslem  24303  fclsfnflim  24346  flimfnfcls  24347  fclscmp  24349  clssubg  24428  tgpconncompeqg  24431  tgpconncomp  24432  qustgpopn  24439  tgptsmscls  24469  xmeter  24752  metust  24877  tgqioo  25119  zcld  25133  iccntr  25141  icccmplem2  25143  icccmplem3  25144  reconnlem1  25146  reconnlem2  25147  xrge0tsms  25154  cnheiborlem  25275  om1addcl  25354  pi1blem  25360  pi1grplem  25370  pi1inv  25373  pi1xfr  25376  pi1xfrcnvlem  25377  pi1coghm  25382  cmetcaulem  25609  ivthlem2  25773  ivthlem3  25774  ovolicc2lem2  25839  ovolicc2lem5  25842  opnmbllem  25922  volcn  25927  ismbf3d  25975  mbfi1fseqlem6  26041  itg2const2  26062  i1fibl  26128  ibladd  26141  bddiblnc  26162  ditgsplitlem  26180  dvferm1lem  26304  dvferm2lem  26306  dvlip2  26315  dvivthlem1  26328  dvne0  26331  lhop1lem  26333  lhop1  26334  lhop  26336  dvcnvrelem1  26337  dvcnvrelem2  26338  dvcnvre  26339  ftc1lem1  26355  itgsubst  26369  aaliou3lem2  26670  psercnlem2  26751  efif1olem2  26871  logtayl  26988  log2tlbnd  27273  xrlimcnp  27296  pntibndlem2  27918  pntlemj  27930  pntleml  27938  bday0b  28199  cuteq0  28201  cuteq1  28203  madebdaylemlrcut  28285  cofcut1  28306  oncutlt  28650  trgcgr  28979  hlid  29075  hltr  29076  btwnhl1  29078  btwnhl2  29079  hlcgrex  29082  mirhl  29151  mirbtwnhl  29152  mirhl2  29153  hlpasch  29234  lnopp2hpgb  29241  cgrahl  29335  axlowdim  29539  uhgrissubgr  29856  egrsubgr  29858  uhgrspansubgr  29872  uhgrspan1  29884  cusgrrusgr  30162  wlkonwlk  30241  wlkonwlk1l  30242  wlkres  30249  wlkp1  30260  wlkd  30265  pfxwlk  30266  revwlk  30267  lfgriswlk  30271  wwlksnextinj  30488  2wlkond  30526  wpthswwlks2on  30553  0wlkon  30711  1wlkd  30732  1pthond  30735  eliccelico  33411  elicoelioo  33412  xrge0tsmsd  33676  tpr2rico  34586  measinb  34896  cntmeas  34901  dya2icoseg  34951  sibf0  35008  sibfof  35014  resconn  36053  cvmsss2  36081  cvmliftlem10  36101  mrsubco  36328  cgrextend  36815  cgr3rflx  36861  cgrxfr  36862  btwnconn1lem4  36897  btwnconn1lem8  36901  btwnconn1lem11  36904  bj-pinftynminfty  38191  bj-rveccmod  38266  iooelexlt  38328  opnmbllem0  38617  ibladdnc  38638  ftc1anc  38662  isbnd3  38761  prdsbnd  38770  rngomndo  38912  isgrpda  38932  rngohomco  38951  rngoisocnv  38958  rngoidl  39001  0idl  39002  intidl  39006  unichnidl  39008  keridl  39009  smprngopr  39029  lshpnel2N  40085  lkrshp  40205  4atexlemex2  41171  4atex  41176  cdleme0moN  41325  istendod  41862  dihlspsnat  42433  dochsatshp  42551  mon1psubm  44244  iocinico  44257  dfrtrcl3  44776  eliood  46553  eliccd  46559  eliocd  46562  limciccioolb  46676  limcicciooub  46690  icccncfext  46940  iblspltprt  47026  itgspltprt  47032  fourierdlem1  47161  fourierdlem4  47164  fourierdlem32  47192  fourierdlem33  47193  fourierdlem43  47203  fourierdlem65  47224  fourierdlem79  47238  prsal  47371  issald  47386  flmrecm1  48456  iccpartrn  48555  fpprwpprb  48881  bgoldbtbnd  48950  upgrimwlk  49043  upgrimpths  49050  gpgedgvtx0  49202  gpgedgvtx1  49203  gpgprismgr4cycllem11  49246  smprngprmrng  49479  expnegico01  49673  dignnld  49758  reorelicc  49865