Theorem mpbir3and 1338

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  canthwelem  10066  intwun  10151  tskwun  10200  gruwun  10229  ixxss1  12750  ixxss2  12751  ixxss12  12752  ixxub  12753  ixxlb  12754  elicod  12781  ubioc1  12784  lbico1  12785  lbicc2  12846  ubicc2  12847  difreicc  12864  supicc  12880  modelico  13243  zmodfz  13255  addmodid  13281  dfrtrcl2  14415  phicl2  16099  4sqlem12  16286  isfuncd  17129  idfucl  17145  cofucl  17152  invfuc  17238  cnvps  17816  psss  17818  issubmd  17965  mndissubm  17966  submid  17969  subsubm  17975  0subm  17976  mhmima  17983  mhmeql  17984  gsumwspan  18005  frmdsssubm  18020  sursubmefmnd  18055  injsubmefmnd  18056  issubgrpd2  18289  grpissubg  18293  subgint  18297  0subg  18298  nmzsubg  18311  eqger  18324  eqgcpbl  18328  cycsubm  18339  cycsubgcl  18343  ghmrn  18365  ghmpreima  18374  gastacl  18433  cntzsubm  18460  sylow2blem1  18739  lsmsubm  18772  torsubg  18968  oddvdssubg  18969  dmdprdd  19115  dprdsubg  19140  dprdres  19144  unitsubm  19414  subrgsubm  19542  subrgugrp  19548  subrgint  19551  issubdrg  19554  cntzsubr  19562  lsssubg  19723  islmhm2  19804  pj1lmhm  19866  islbs2  19920  islbs3  19921  lbsextlem4  19927  issubrngd2  19955  lidlsubg  19982  2idlcpbl  20001  mplsubglem  20208  mplsubrg  20214  mplind  20276  mhpsubg  20334  isphld  20792  dmatsgrp  21102  dmatsrng  21104  scmatsgrp  21122  scmatsrng  21123  scmatsgrp1  21125  scmatsrng1  21126  cpmatsubgpmat  21322  cpmatsrgpmat  21323  lmcnp  21906  isufil2  22510  ufileu  22521  filufint  22522  fmfnfm  22560  flimclslem  22586  fclsfnflim  22629  flimfnfcls  22630  fclscmp  22632  clssubg  22711  tgpconncompeqg  22714  tgpconncomp  22715  qustgpopn  22722  tgptsmscls  22752  xmeter  23037  metust  23162  tgqioo  23402  zcld  23415  iccntr  23423  icccmplem2  23425  icccmplem3  23426  reconnlem1  23428  reconnlem2  23429  xrge0tsms  23436  cnheiborlem  23552  om1addcl  23631  pi1blem  23637  pi1grplem  23647  pi1inv  23650  pi1xfr  23653  pi1xfrcnvlem  23654  pi1coghm  23659  cmetcaulem  23885  ivthlem2  24047  ivthlem3  24048  ovolicc2lem2  24113  ovolicc2lem5  24116  opnmbllem  24196  volcn  24201  ismbf3d  24249  mbfi1fseqlem6  24315  itg2const2  24336  i1fibl  24402  ibladd  24415  ditgsplitlem  24452  dvferm1lem  24575  dvferm2lem  24577  dvlip2  24586  dvivthlem1  24599  dvne0  24602  lhop1lem  24604  lhop1  24605  lhop  24607  dvcnvrelem1  24608  dvcnvrelem2  24609  dvcnvre  24610  ftc1lem1  24626  itgsubst  24640  aaliou3lem2  24926  psercnlem2  25006  efif1olem2  25121  logtayl  25237  log2tlbnd  25517  xrlimcnp  25540  pntibndlem2  26161  pntlemj  26173  pntleml  26181  trgcgr  26296  hlid  26389  hltr  26390  btwnhl1  26392  btwnhl2  26393  hlcgrex  26396  mirhl  26459  mirbtwnhl  26460  mirhl2  26461  hlpasch  26536  lnopp2hpgb  26543  cgrahl  26607  axlowdim  26741  uhgrissubgr  27051  egrsubgr  27053  uhgrspansubgr  27067  uhgrspan1  27079  cusgrrusgr  27357  wlkonwlk  27438  wlkonwlk1l  27439  wlkres  27446  wlkp1  27457  wlkd  27462  lfgriswlk  27464  wwlksnextinj  27671  2wlkond  27710  wpthswwlks2on  27734  0wlkon  27893  1wlkd  27914  1pthond  27917  eliccelico  30494  elicoelioo  30495  xrge0tsmsd  30687  tpr2rico  31150  measinb  31475  cntmeas  31480  dya2icoseg  31530  sibf0  31587  sibfof  31593  pfxwlk  32365  revwlk  32366  resconn  32488  cvmsss2  32516  cvmliftlem10  32536  mrsubco  32763  cgrextend  33464  cgr3rflx  33510  cgrxfr  33511  btwnconn1lem4  33546  btwnconn1lem8  33550  btwnconn1lem11  33553  bj-pinftynminfty  34503  bj-rveccmod  34577  iooelexlt  34637  opnmbllem0  34922  ibladdnc  34943  bddiblnc  34956  ftc1anc  34969  isbnd3  35056  prdsbnd  35065  rngomndo  35207  isgrpda  35227  rngohomco  35246  rngoisocnv  35253  rngoidl  35296  0idl  35297  intidl  35301  unichnidl  35303  keridl  35304  smprngopr  35324  lshpnel2N  36115  lkrshp  36235  4atexlemex2  37201  4atex  37206  cdleme0moN  37355  istendod  37892  dihlspsnat  38463  dochsatshp  38581  mon1psubm  39799  iocinico  39811  dfrtrcl3  40071  eliood  41766  eliccd  41772  eliocd  41776  limciccioolb  41895  limcicciooub  41911  icccncfext  42163  iblspltprt  42251  itgspltprt  42257  fourierdlem1  42387  fourierdlem4  42390  fourierdlem32  42418  fourierdlem33  42419  fourierdlem43  42429  fourierdlem65  42450  fourierdlem79  42464  prsal  42597  issald  42610  iccpartrn  43584  fpprwpprb  43899  bgoldbtbnd  43968  expnegico01  44567  dignnld  44657  reorelicc  44691