Theorem mpbir3and 1339

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  2ellim  8518  canthwelem  10673  intwun  10758  tskwun  10807  gruwun  10836  ixxss1  13374  ixxss2  13375  ixxss12  13376  ixxub  13377  ixxlb  13378  elicod  13406  ubioc1  13409  lbico1  13410  lbicc2  13473  ubicc2  13474  difreicc  13493  supicc  13510  modelico  13878  zmodfz  13890  addmodid  13916  dfrtrcl2  15041  phicl2  16736  4sqlem12  16924  isfuncd  17850  idfucl  17866  cofucl  17873  invfuc  17965  cnvps  18569  psss  18571  issubmd  18762  mndissubm  18763  submid  18766  subsubm  18772  0subm  18773  mhmima  18781  mhmeql  18782  gsumwspan  18802  frmdsssubm  18817  sursubmefmnd  18852  injsubmefmnd  18853  issubgrpd2  19101  grpissubg  19105  subgint  19109  0subgOLD  19111  nmzsubg  19124  eqger  19137  eqgcpbl  19141  cycsubm  19161  cycsubgcl  19165  ghmrn  19187  ghmpreima  19196  gastacl  19264  cntzsubm  19293  sylow2blem1  19579  lsmsubm  19612  torsubg  19813  oddvdssubg  19814  dmdprdd  19960  dprdsubg  19985  dprdres  19989  unitsubm  20329  cntzsubrng  20508  subrgsubm  20528  subrgugrp  20534  subrgint  20538  cntzsubr  20549  issubdrg  20672  lsssubg  20845  islmhm2  20927  pj1lmhm  20989  islbs2  21046  islbs3  21047  lbsextlem4  21053  issubrgd  21086  lidlsubg  21123  2idlcpblrng  21169  isphld  21590  mplsubglem  21948  mplsubrg  21954  mplind  22021  mhpsubg  22085  dmatsgrp  22431  dmatsrng  22433  scmatsgrp  22451  scmatsrng  22452  scmatsgrp1  22454  scmatsrng1  22455  cpmatsubgpmat  22652  cpmatsrgpmat  22653  lmcnp  23238  isufil2  23842  ufileu  23853  filufint  23854  fmfnfm  23892  flimclslem  23918  fclsfnflim  23961  flimfnfcls  23962  fclscmp  23964  clssubg  24043  tgpconncompeqg  24046  tgpconncomp  24047  qustgpopn  24054  tgptsmscls  24084  xmeter  24369  metust  24497  tgqioo  24746  zcld  24759  iccntr  24767  icccmplem2  24769  icccmplem3  24770  reconnlem1  24772  reconnlem2  24773  xrge0tsms  24780  cnheiborlem  24910  om1addcl  24990  pi1blem  24996  pi1grplem  25006  pi1inv  25009  pi1xfr  25012  pi1xfrcnvlem  25013  pi1coghm  25018  cmetcaulem  25246  ivthlem2  25411  ivthlem3  25412  ovolicc2lem2  25477  ovolicc2lem5  25480  opnmbllem  25560  volcn  25565  ismbf3d  25613  mbfi1fseqlem6  25680  itg2const2  25701  i1fibl  25767  ibladd  25780  bddiblnc  25801  ditgsplitlem  25819  dvferm1lem  25946  dvferm2lem  25948  dvlip2  25958  dvivthlem1  25971  dvne0  25974  lhop1lem  25976  lhop1  25977  lhop  25979  dvcnvrelem1  25980  dvcnvrelem2  25981  dvcnvre  25982  ftc1lem1  26000  itgsubst  26014  aaliou3lem2  26308  psercnlem2  26391  efif1olem2  26507  logtayl  26624  log2tlbnd  26907  xrlimcnp  26930  pntibndlem2  27554  pntlemj  27566  pntleml  27574  bday0b  27793  cuteq0  27795  cuteq1  27796  madebdaylemlrcut  27855  cofcut1  27870  trgcgr  28376  hlid  28469  hltr  28470  btwnhl1  28472  btwnhl2  28473  hlcgrex  28476  mirhl  28539  mirbtwnhl  28540  mirhl2  28541  hlpasch  28616  lnopp2hpgb  28623  cgrahl  28687  axlowdim  28828  uhgrissubgr  29144  egrsubgr  29146  uhgrspansubgr  29160  uhgrspan1  29172  cusgrrusgr  29451  wlkonwlk  29532  wlkonwlk1l  29533  wlkres  29540  wlkp1  29551  wlkd  29556  lfgriswlk  29558  wwlksnextinj  29766  2wlkond  29804  wpthswwlks2on  29828  0wlkon  29986  1wlkd  30007  1pthond  30010  eliccelico  32602  elicoelioo  32603  xrge0tsmsd  32828  tpr2rico  33583  measinb  33910  cntmeas  33915  dya2icoseg  33967  sibf0  34024  sibfof  34030  pfxwlk  34803  revwlk  34804  resconn  34926  cvmsss2  34954  cvmliftlem10  34974  mrsubco  35201  cgrextend  35674  cgr3rflx  35720  cgrxfr  35721  btwnconn1lem4  35756  btwnconn1lem8  35760  btwnconn1lem11  35763  bj-pinftynminfty  36776  bj-rveccmod  36851  iooelexlt  36911  opnmbllem0  37199  ibladdnc  37220  ftc1anc  37244  isbnd3  37327  prdsbnd  37336  rngomndo  37478  isgrpda  37498  rngohomco  37517  rngoisocnv  37524  rngoidl  37567  0idl  37568  intidl  37572  unichnidl  37574  keridl  37575  smprngopr  37595  lshpnel2N  38526  lkrshp  38646  4atexlemex2  39613  4atex  39618  cdleme0moN  39767  istendod  40304  dihlspsnat  40875  dochsatshp  40993  mon1psubm  42692  iocinico  42705  dfrtrcl3  43228  eliood  44946  eliccd  44952  eliocd  44955  limciccioolb  45072  limcicciooub  45088  icccncfext  45338  iblspltprt  45424  itgspltprt  45430  fourierdlem1  45559  fourierdlem4  45562  fourierdlem32  45590  fourierdlem33  45591  fourierdlem43  45601  fourierdlem65  45622  fourierdlem79  45636  prsal  45769  issald  45784  iccpartrn  46833  fpprwpprb  47143  bgoldbtbnd  47212  expnegico01  47698  dignnld  47788  reorelicc  47895