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  8485  canthwelem  10706  intwun  10791  tskwun  10840  gruwun  10869  ixxss1  13463  ixxss2  13464  ixxss12  13465  ixxub  13466  ixxlb  13467  elicod  13495  ubioc1  13499  lbico1  13500  lbicc2  13564  ubicc2  13565  difreicc  13584  supicc  13601  nnge2recico01  13607  modelico  13989  zmodfz  14001  addmodid  14030  dfrtrcl2  15182  phicl2  16906  4sqlem12  17095  isfuncd  18001  idfucl  18017  cofucl  18024  invfuc  18113  cnvps  18713  psss  18715  issubmd  18962  mndissubm  18963  submid  18966  subsubm  18973  0subm  18974  mhmima  18982  mhmeql  18983  gsumwspan  19003  frmdsssubm  19018  sursubmefmnd  19053  injsubmefmnd  19054  issubgrpd2  19314  grpissubg  19318  subgint  19322  nmzsubg  19336  eqger  19351  eqgcpbl  19355  cycsubm  19378  cycsubgcl  19382  ghmrn  19404  ghmpreima  19413  gastacl  19484  cntzsubm  19513  sylow2blem1  19795  lsmsubm  19828  torsubg  20029  oddvdssubg  20030  dmdprdd  20176  dprdsubg  20201  dprdres  20205  unitsubm  20577  cntzsubrng  20780  subrgsubm  20798  subrgugrp  20804  subrgint  20808  cntzsubr  20819  issubdrg  20998  lsssubg  21193  islmhm2  21274  pj1lmhm  21336  islbs2  21393  islbs3  21394  lbsextlem4  21400  issubrgd  21425  lidlsubg  21463  2idlcpblrng  21526  isphld  21921  mplsubglem  22267  mplsubrg  22273  mplind  22340  mhpsubg  22435  dmatsgrp  22775  dmatsrng  22777  scmatsgrp  22795  scmatsrng  22796  scmatsgrp1  22798  scmatsrng1  22799  cpmatsubgpmat  22999  cpmatsrgpmat  23000  lmcnp  23583  isufil2  24188  ufileu  24199  filufint  24200  fmfnfm  24238  flimclslem  24264  fclsfnflim  24307  flimfnfcls  24308  fclscmp  24310  clssubg  24389  tgpconncompeqg  24392  tgpconncomp  24393  qustgpopn  24400  tgptsmscls  24430  xmeter  24713  metust  24838  tgqioo  25080  zcld  25094  iccntr  25102  icccmplem2  25104  icccmplem3  25105  reconnlem1  25107  reconnlem2  25108  xrge0tsms  25115  cnheiborlem  25236  om1addcl  25315  pi1blem  25321  pi1grplem  25331  pi1inv  25334  pi1xfr  25337  pi1xfrcnvlem  25338  pi1coghm  25343  cmetcaulem  25570  ivthlem2  25734  ivthlem3  25735  ovolicc2lem2  25800  ovolicc2lem5  25803  opnmbllem  25883  volcn  25888  ismbf3d  25936  mbfi1fseqlem6  26002  itg2const2  26023  i1fibl  26089  ibladd  26102  bddiblnc  26123  ditgsplitlem  26141  dvferm1lem  26265  dvferm2lem  26267  dvlip2  26276  dvivthlem1  26289  dvne0  26292  lhop1lem  26294  lhop1  26295  lhop  26297  dvcnvrelem1  26298  dvcnvrelem2  26299  dvcnvre  26300  ftc1lem1  26316  itgsubst  26330  aaliou3lem2  26633  psercnlem2  26714  efif1olem2  26834  logtayl  26951  log2tlbnd  27236  xrlimcnp  27259  pntibndlem2  27881  pntlemj  27893  pntleml  27901  bday0b  28132  cuteq0  28134  cuteq1  28136  madebdaylemlrcut  28218  cofcut1  28239  oncutlt  28583  trgcgr  28912  hlid  29008  hltr  29009  btwnhl1  29011  btwnhl2  29012  hlcgrex  29015  mirhl  29084  mirbtwnhl  29085  mirhl2  29086  hlpasch  29167  lnopp2hpgb  29174  cgrahl  29268  axlowdim  29472  uhgrissubgr  29789  egrsubgr  29791  uhgrspansubgr  29805  uhgrspan1  29817  cusgrrusgr  30095  wlkonwlk  30174  wlkonwlk1l  30175  wlkres  30182  wlkp1  30193  wlkd  30198  pfxwlk  30199  revwlk  30200  lfgriswlk  30204  wwlksnextinj  30421  2wlkond  30459  wpthswwlks2on  30486  0wlkon  30644  1wlkd  30665  1pthond  30668  eliccelico  33302  elicoelioo  33303  xrge0tsmsd  33567  tpr2rico  34477  measinb  34787  cntmeas  34792  dya2icoseg  34843  sibf0  34900  sibfof  34906  resconn  35932  cvmsss2  35960  cvmliftlem10  35980  mrsubco  36207  cgrextend  36695  cgr3rflx  36741  cgrxfr  36742  btwnconn1lem4  36777  btwnconn1lem8  36781  btwnconn1lem11  36784  bj-pinftynminfty  38068  bj-rveccmod  38143  iooelexlt  38205  opnmbllem0  38494  ibladdnc  38515  ftc1anc  38539  isbnd3  38638  prdsbnd  38647  rngomndo  38789  isgrpda  38809  rngohomco  38828  rngoisocnv  38835  rngoidl  38878  0idl  38879  intidl  38883  unichnidl  38885  keridl  38886  smprngopr  38906  lshpnel2N  39962  lkrshp  40082  4atexlemex2  41048  4atex  41053  cdleme0moN  41202  istendod  41739  dihlspsnat  42310  dochsatshp  42428  mon1psubm  44144  iocinico  44157  dfrtrcl3  44677  eliood  46432  eliccd  46438  eliocd  46441  limciccioolb  46555  limcicciooub  46569  icccncfext  46819  iblspltprt  46905  itgspltprt  46911  fourierdlem1  47040  fourierdlem4  47043  fourierdlem32  47071  fourierdlem33  47072  fourierdlem43  47082  fourierdlem65  47103  fourierdlem79  47117  prsal  47250  issald  47265  flmrecm1  48335  iccpartrn  48434  fpprwpprb  48760  bgoldbtbnd  48829  upgrimwlk  48922  upgrimpths  48929  gpgedgvtx0  49081  gpgedgvtx1  49082  gpgprismgr4cycllem11  49125  smprngprmrng  49358  expnegico01  49552  dignnld  49637  reorelicc  49744