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  8535  canthwelem  10762  intwun  10847  tskwun  10896  gruwun  10925  ixxss1  13521  ixxss2  13522  ixxss12  13523  ixxub  13524  ixxlb  13525  elicod  13553  ubioc1  13557  lbico1  13558  lbicc2  13622  ubicc2  13623  difreicc  13642  supicc  13659  nnge2recico01  13665  modelico  14048  zmodfz  14060  addmodid  14089  dfrtrcl2  15244  phicl2  16974  4sqlem12  17163  isfuncd  18069  idfucl  18085  cofucl  18092  invfuc  18181  cnvps  18781  psss  18783  issubmd  19030  mndissubm  19031  submid  19034  subsubm  19041  0subm  19042  mhmima  19050  mhmeql  19051  gsumwspan  19071  frmdsssubm  19086  sursubmefmnd  19121  injsubmefmnd  19122  issubgrpd2  19382  grpissubg  19386  subgint  19390  nmzsubg  19404  eqger  19419  eqgcpbl  19423  cycsubm  19446  cycsubgcl  19450  ghmrn  19472  ghmpreima  19481  gastacl  19553  cntzsubm  19582  sylow2blem1  19864  lsmsubm  19897  torsubg  20098  oddvdssubg  20099  dmdprdd  20245  dprdsubg  20270  dprdres  20274  unitsubm  20646  cntzsubrng  20849  subrgsubm  20867  subrgugrp  20873  subrgint  20877  cntzsubr  20888  issubdrg  21067  lsssubg  21262  islmhm2  21343  pj1lmhm  21405  islbs2  21462  islbs3  21463  lbsextlem4  21469  issubrgd  21494  lidlsubg  21532  2idlcpblrng  21595  isphld  21990  mplsubglem  22336  mplsubrg  22342  mplind  22409  mhpsubg  22504  dmatsgrp  22844  dmatsrng  22846  scmatsgrp  22864  scmatsrng  22865  scmatsgrp1  22867  scmatsrng1  22868  cpmatsubgpmat  23068  cpmatsrgpmat  23069  lmcnp  23652  isufil2  24257  ufileu  24268  filufint  24269  fmfnfm  24307  flimclslem  24333  fclsfnflim  24376  flimfnfcls  24377  fclscmp  24379  clssubg  24458  tgpconncompeqg  24461  tgpconncomp  24462  qustgpopn  24469  tgptsmscls  24499  xmeter  24782  metust  24907  tgqioo  25149  zcld  25163  iccntr  25171  icccmplem2  25173  icccmplem3  25174  reconnlem1  25176  reconnlem2  25177  xrge0tsms  25184  cnheiborlem  25305  om1addcl  25384  pi1blem  25390  pi1grplem  25400  pi1inv  25403  pi1xfr  25406  pi1xfrcnvlem  25407  pi1coghm  25412  cmetcaulem  25639  ivthlem2  25803  ivthlem3  25804  ovolicc2lem2  25869  ovolicc2lem5  25872  opnmbllem  25952  volcn  25957  ismbf3d  26005  mbfi1fseqlem6  26071  itg2const2  26092  i1fibl  26158  ibladd  26171  bddiblnc  26192  ditgsplitlem  26210  dvferm1lem  26334  dvferm2lem  26336  dvlip2  26345  dvivthlem1  26358  dvne0  26361  lhop1lem  26363  lhop1  26364  lhop  26366  dvcnvrelem1  26367  dvcnvrelem2  26368  dvcnvre  26369  ftc1lem1  26385  itgsubst  26399  aaliou3lem2  26700  psercnlem2  26781  efif1olem2  26901  logtayl  27018  log2tlbnd  27303  xrlimcnp  27326  pntibndlem2  27948  pntlemj  27960  pntleml  27968  bday0b  28229  cuteq0  28231  cuteq1  28233  madebdaylemlrcut  28315  cofcut1  28336  oncutlt  28680  trgcgr  29009  hlid  29105  hltr  29106  btwnhl1  29108  btwnhl2  29109  hlcgrex  29112  mirhl  29181  mirbtwnhl  29182  mirhl2  29183  hlpasch  29264  lnopp2hpgb  29271  cgrahl  29365  axlowdim  29569  uhgrissubgr  29886  egrsubgr  29888  uhgrspansubgr  29902  uhgrspan1  29914  cusgrrusgr  30192  wlkonwlk  30271  wlkonwlk1l  30272  wlkres  30279  wlkp1  30290  wlkd  30295  pfxwlk  30296  revwlk  30297  lfgriswlk  30301  wwlksnextinj  30518  2wlkond  30556  wpthswwlks2on  30583  0wlkon  30741  1wlkd  30762  1pthond  30765  eliccelico  33439  elicoelioo  33440  xrge0tsmsd  33704  tpr2rico  34614  measinb  34924  cntmeas  34929  dya2icoseg  34979  sibf0  35036  sibfof  35042  resconn  36178  cvmsss2  36206  cvmliftlem10  36226  mrsubco  36453  cgrextend  36951  cgr3rflx  36997  cgrxfr  36998  btwnconn1lem4  37033  btwnconn1lem8  37037  btwnconn1lem11  37040  bj-pinftynminfty  38340  bj-rveccmod  38415  iooelexlt  38477  opnmbllem0  38766  ibladdnc  38787  ftc1anc  38811  isbnd3  38910  prdsbnd  38919  rngomndo  39061  isgrpda  39081  rngohomco  39100  rngoisocnv  39107  rngoidl  39150  0idl  39151  intidl  39155  unichnidl  39157  keridl  39158  smprngopr  39178  lshpnel2N  40234  lkrshp  40354  4atexlemex2  41320  4atex  41325  cdleme0moN  41474  istendod  42011  dihlspsnat  42582  dochsatshp  42700  mon1psubm  44393  iocinico  44406  dfrtrcl3  44925  eliood  46715  eliccd  46721  eliocd  46724  limciccioolb  46838  limcicciooub  46852  icccncfext  47102  iblspltprt  47188  itgspltprt  47194  fourierdlem1  47323  fourierdlem4  47326  fourierdlem32  47354  fourierdlem33  47355  fourierdlem43  47365  fourierdlem65  47386  fourierdlem79  47400  prsal  47533  issald  47548  flmrecm1  48618  iccpartrn  48717  fpprwpprb  49043  bgoldbtbnd  49112  upgrimwlk  49205  upgrimpths  49212  gpgedgvtx0  49364  gpgedgvtx1  49365  gpgprismgr4cycllem11  49408  smprngprmrng  49641  expnegico01  49835  dignnld  49920  reorelicc  50027