Theorem mpbir3and 1344

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 206   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  2ellim  8425  canthwelem  10562  intwun  10647  tskwun  10696  gruwun  10725  ixxss1  13280  ixxss2  13281  ixxss12  13282  ixxub  13283  ixxlb  13284  elicod  13312  ubioc1  13316  lbico1  13317  lbicc2  13381  ubicc2  13382  difreicc  13401  supicc  13418  modelico  13802  zmodfz  13814  addmodid  13843  dfrtrcl2  14986  phicl2  16696  4sqlem12  16885  isfuncd  17790  idfucl  17806  cofucl  17813  invfuc  17902  cnvps  18502  psss  18504  issubmd  18732  mndissubm  18733  submid  18736  subsubm  18742  0subm  18743  mhmima  18751  mhmeql  18752  gsumwspan  18772  frmdsssubm  18787  sursubmefmnd  18822  injsubmefmnd  18823  issubgrpd2  19076  grpissubg  19080  subgint  19084  nmzsubg  19098  eqger  19111  eqgcpbl  19115  cycsubm  19135  cycsubgcl  19139  ghmrn  19162  ghmpreima  19171  gastacl  19242  cntzsubm  19271  sylow2blem1  19553  lsmsubm  19586  torsubg  19787  oddvdssubg  19788  dmdprdd  19934  dprdsubg  19959  dprdres  19963  unitsubm  20324  cntzsubrng  20502  subrgsubm  20520  subrgugrp  20526  subrgint  20530  cntzsubr  20541  issubdrg  20715  lsssubg  20910  islmhm2  20992  pj1lmhm  21054  islbs2  21111  islbs3  21112  lbsextlem4  21118  issubrgd  21143  lidlsubg  21180  2idlcpblrng  21228  isphld  21611  mplsubglem  21955  mplsubrg  21961  mplind  22026  mhpsubg  22097  dmatsgrp  22442  dmatsrng  22444  scmatsgrp  22462  scmatsrng  22463  scmatsgrp1  22465  scmatsrng1  22466  cpmatsubgpmat  22663  cpmatsrgpmat  22664  lmcnp  23247  isufil2  23851  ufileu  23862  filufint  23863  fmfnfm  23901  flimclslem  23927  fclsfnflim  23970  flimfnfcls  23971  fclscmp  23973  clssubg  24052  tgpconncompeqg  24055  tgpconncomp  24056  qustgpopn  24063  tgptsmscls  24093  xmeter  24376  metust  24501  tgqioo  24743  zcld  24757  iccntr  24765  icccmplem2  24767  icccmplem3  24768  reconnlem1  24770  reconnlem2  24771  xrge0tsms  24778  cnheiborlem  24899  om1addcl  24978  pi1blem  24984  pi1grplem  24994  pi1inv  24997  pi1xfr  25000  pi1xfrcnvlem  25001  pi1coghm  25006  cmetcaulem  25233  ivthlem2  25397  ivthlem3  25398  ovolicc2lem2  25463  ovolicc2lem5  25466  opnmbllem  25546  volcn  25551  ismbf3d  25599  mbfi1fseqlem6  25665  itg2const2  25686  i1fibl  25753  ibladd  25766  bddiblnc  25787  ditgsplitlem  25805  dvferm1lem  25929  dvferm2lem  25931  dvlip2  25941  dvivthlem1  25954  dvne0  25957  lhop1lem  25959  lhop1  25960  lhop  25962  dvcnvrelem1  25963  dvcnvrelem2  25964  dvcnvre  25965  ftc1lem1  25983  itgsubst  25997  aaliou3lem2  26291  psercnlem2  26374  efif1olem2  26492  logtayl  26609  log2tlbnd  26895  xrlimcnp  26918  pntibndlem2  27542  pntlemj  27554  pntleml  27562  bday0b  27793  cuteq0  27795  cuteq1  27797  madebdaylemlrcut  27879  cofcut1  27900  oncutlt  28244  trgcgr  28572  hlid  28665  hltr  28666  btwnhl1  28668  btwnhl2  28669  hlcgrex  28672  mirhl  28735  mirbtwnhl  28736  mirhl2  28737  hlpasch  28812  lnopp2hpgb  28819  cgrahl  28883  axlowdim  29018  uhgrissubgr  29332  egrsubgr  29334  uhgrspansubgr  29348  uhgrspan1  29360  cusgrrusgr  29639  wlkonwlk  29718  wlkonwlk1l  29719  wlkres  29726  wlkp1  29737  wlkd  29742  lfgriswlk  29744  wwlksnextinj  29956  2wlkond  29994  wpthswwlks2on  30021  0wlkon  30179  1wlkd  30200  1pthond  30203  eliccelico  32840  elicoelioo  32841  xrge0tsmsd  33139  tpr2rico  34062  measinb  34371  cntmeas  34376  dya2icoseg  34427  sibf0  34484  sibfof  34490  pfxwlk  35312  revwlk  35313  resconn  35434  cvmsss2  35462  cvmliftlem10  35482  mrsubco  35709  cgrextend  36196  cgr3rflx  36242  cgrxfr  36243  btwnconn1lem4  36278  btwnconn1lem8  36282  btwnconn1lem11  36285  bj-pinftynminfty  37539  bj-rveccmod  37614  iooelexlt  37674  opnmbllem0  37968  ibladdnc  37989  ftc1anc  38013  isbnd3  38096  prdsbnd  38105  rngomndo  38247  isgrpda  38267  rngohomco  38286  rngoisocnv  38293  rngoidl  38336  0idl  38337  intidl  38341  unichnidl  38343  keridl  38344  smprngopr  38364  lshpnel2N  39422  lkrshp  39542  4atexlemex2  40508  4atex  40513  cdleme0moN  40662  istendod  41199  dihlspsnat  41770  dochsatshp  41888  mon1psubm  43630  iocinico  43643  dfrtrcl3  44163  eliood  45932  eliccd  45938  eliocd  45941  limciccioolb  46055  limcicciooub  46069  icccncfext  46319  iblspltprt  46405  itgspltprt  46411  fourierdlem1  46540  fourierdlem4  46543  fourierdlem32  46571  fourierdlem33  46572  fourierdlem43  46582  fourierdlem65  46603  fourierdlem79  46617  prsal  46750  issald  46765  iccpartrn  47864  fpprwpprb  48174  bgoldbtbnd  48243  upgrimwlk  48336  upgrimpths  48343  gpgedgvtx0  48495  gpgedgvtx1  48496  gpgprismgr4cycllem11  48539  expnegico01  48952  dignnld  49037  reorelicc  49144