Theorem mpbir3and 1343

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086

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 1088

This theorem is referenced by:  2ellim  8466  canthwelem  10610  intwun  10695  tskwun  10744  gruwun  10773  ixxss1  13331  ixxss2  13332  ixxss12  13333  ixxub  13334  ixxlb  13335  elicod  13363  ubioc1  13367  lbico1  13368  lbicc2  13432  ubicc2  13433  difreicc  13452  supicc  13469  modelico  13850  zmodfz  13862  addmodid  13891  dfrtrcl2  15035  phicl2  16745  4sqlem12  16934  isfuncd  17834  idfucl  17850  cofucl  17857  invfuc  17946  cnvps  18544  psss  18546  issubmd  18740  mndissubm  18741  submid  18744  subsubm  18750  0subm  18751  mhmima  18759  mhmeql  18760  gsumwspan  18780  frmdsssubm  18795  sursubmefmnd  18830  injsubmefmnd  18831  issubgrpd2  19081  grpissubg  19085  subgint  19089  0subgOLD  19091  nmzsubg  19104  eqger  19117  eqgcpbl  19121  cycsubm  19141  cycsubgcl  19145  ghmrn  19168  ghmpreima  19177  gastacl  19248  cntzsubm  19277  sylow2blem1  19557  lsmsubm  19590  torsubg  19791  oddvdssubg  19792  dmdprdd  19938  dprdsubg  19963  dprdres  19967  unitsubm  20302  cntzsubrng  20483  subrgsubm  20501  subrgugrp  20507  subrgint  20511  cntzsubr  20522  issubdrg  20696  lsssubg  20870  islmhm2  20952  pj1lmhm  21014  islbs2  21071  islbs3  21072  lbsextlem4  21078  issubrgd  21103  lidlsubg  21140  2idlcpblrng  21188  isphld  21570  mplsubglem  21915  mplsubrg  21921  mplind  21984  mhpsubg  22047  dmatsgrp  22393  dmatsrng  22395  scmatsgrp  22413  scmatsrng  22414  scmatsgrp1  22416  scmatsrng1  22417  cpmatsubgpmat  22614  cpmatsrgpmat  22615  lmcnp  23198  isufil2  23802  ufileu  23813  filufint  23814  fmfnfm  23852  flimclslem  23878  fclsfnflim  23921  flimfnfcls  23922  fclscmp  23924  clssubg  24003  tgpconncompeqg  24006  tgpconncomp  24007  qustgpopn  24014  tgptsmscls  24044  xmeter  24328  metust  24453  tgqioo  24695  zcld  24709  iccntr  24717  icccmplem2  24719  icccmplem3  24720  reconnlem1  24722  reconnlem2  24723  xrge0tsms  24730  cnheiborlem  24860  om1addcl  24940  pi1blem  24946  pi1grplem  24956  pi1inv  24959  pi1xfr  24962  pi1xfrcnvlem  24963  pi1coghm  24968  cmetcaulem  25195  ivthlem2  25360  ivthlem3  25361  ovolicc2lem2  25426  ovolicc2lem5  25429  opnmbllem  25509  volcn  25514  ismbf3d  25562  mbfi1fseqlem6  25628  itg2const2  25649  i1fibl  25716  ibladd  25729  bddiblnc  25750  ditgsplitlem  25768  dvferm1lem  25895  dvferm2lem  25897  dvlip2  25907  dvivthlem1  25920  dvne0  25923  lhop1lem  25925  lhop1  25926  lhop  25928  dvcnvrelem1  25929  dvcnvrelem2  25930  dvcnvre  25931  ftc1lem1  25949  itgsubst  25963  aaliou3lem2  26258  psercnlem2  26341  efif1olem2  26459  logtayl  26576  log2tlbnd  26862  xrlimcnp  26885  pntibndlem2  27509  pntlemj  27521  pntleml  27529  bday0b  27749  cuteq0  27751  cuteq1  27753  madebdaylemlrcut  27817  cofcut1  27835  onscutlt  28172  trgcgr  28450  hlid  28543  hltr  28544  btwnhl1  28546  btwnhl2  28547  hlcgrex  28550  mirhl  28613  mirbtwnhl  28614  mirhl2  28615  hlpasch  28690  lnopp2hpgb  28697  cgrahl  28761  axlowdim  28895  uhgrissubgr  29209  egrsubgr  29211  uhgrspansubgr  29225  uhgrspan1  29237  cusgrrusgr  29516  wlkonwlk  29597  wlkonwlk1l  29598  wlkres  29605  wlkp1  29616  wlkd  29621  lfgriswlk  29623  wwlksnextinj  29836  2wlkond  29874  wpthswwlks2on  29898  0wlkon  30056  1wlkd  30077  1pthond  30080  eliccelico  32707  elicoelioo  32708  xrge0tsmsd  33009  tpr2rico  33909  measinb  34218  cntmeas  34223  dya2icoseg  34275  sibf0  34332  sibfof  34338  pfxwlk  35118  revwlk  35119  resconn  35240  cvmsss2  35268  cvmliftlem10  35288  mrsubco  35515  cgrextend  36003  cgr3rflx  36049  cgrxfr  36050  btwnconn1lem4  36085  btwnconn1lem8  36089  btwnconn1lem11  36092  bj-pinftynminfty  37222  bj-rveccmod  37297  iooelexlt  37357  opnmbllem0  37657  ibladdnc  37678  ftc1anc  37702  isbnd3  37785  prdsbnd  37794  rngomndo  37936  isgrpda  37956  rngohomco  37975  rngoisocnv  37982  rngoidl  38025  0idl  38026  intidl  38030  unichnidl  38032  keridl  38033  smprngopr  38053  lshpnel2N  38985  lkrshp  39105  4atexlemex2  40072  4atex  40077  cdleme0moN  40226  istendod  40763  dihlspsnat  41334  dochsatshp  41452  mon1psubm  43195  iocinico  43208  dfrtrcl3  43729  eliood  45503  eliccd  45509  eliocd  45512  limciccioolb  45626  limcicciooub  45642  icccncfext  45892  iblspltprt  45978  itgspltprt  45984  fourierdlem1  46113  fourierdlem4  46116  fourierdlem32  46144  fourierdlem33  46145  fourierdlem43  46155  fourierdlem65  46176  fourierdlem79  46190  prsal  46323  issald  46338  iccpartrn  47435  fpprwpprb  47745  bgoldbtbnd  47814  upgrimwlk  47906  upgrimpths  47913  gpgedgvtx0  48056  gpgedgvtx1  48057  gpgprismgr4cycllem11  48099  expnegico01  48511  dignnld  48596  reorelicc  48703