Theorem mpbir3and 1342

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 205   ∧ 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 206  df-an 398  df-3an 1089

This theorem is referenced by:  2ellim  8360  canthwelem  10452  intwun  10537  tskwun  10586  gruwun  10615  ixxss1  13143  ixxss2  13144  ixxss12  13145  ixxub  13146  ixxlb  13147  elicod  13175  ubioc1  13178  lbico1  13179  lbicc2  13242  ubicc2  13243  difreicc  13262  supicc  13279  modelico  13647  zmodfz  13659  addmodid  13685  dfrtrcl2  14818  phicl2  16514  4sqlem12  16702  isfuncd  17625  idfucl  17641  cofucl  17648  invfuc  17737  cnvps  18341  psss  18343  issubmd  18490  mndissubm  18491  submid  18494  subsubm  18500  0subm  18501  mhmima  18508  mhmeql  18509  gsumwspan  18530  frmdsssubm  18545  sursubmefmnd  18580  injsubmefmnd  18581  issubgrpd2  18816  grpissubg  18820  subgint  18824  0subg  18825  nmzsubg  18838  eqger  18851  eqgcpbl  18855  cycsubm  18866  cycsubgcl  18870  ghmrn  18892  ghmpreima  18901  gastacl  18960  cntzsubm  18987  sylow2blem1  19270  lsmsubm  19303  torsubg  19500  oddvdssubg  19501  dmdprdd  19647  dprdsubg  19672  dprdres  19676  unitsubm  19957  subrgsubm  20082  subrgugrp  20088  subrgint  20091  issubdrg  20094  cntzsubr  20102  lsssubg  20264  islmhm2  20345  pj1lmhm  20407  islbs2  20461  islbs3  20462  lbsextlem4  20468  issubrngd2  20504  lidlsubg  20531  2idlcpbl  20550  isphld  20904  mplsubglem  21250  mplsubrg  21256  mplind  21323  mhpsubg  21388  dmatsgrp  21693  dmatsrng  21695  scmatsgrp  21713  scmatsrng  21714  scmatsgrp1  21716  scmatsrng1  21717  cpmatsubgpmat  21914  cpmatsrgpmat  21915  lmcnp  22500  isufil2  23104  ufileu  23115  filufint  23116  fmfnfm  23154  flimclslem  23180  fclsfnflim  23223  flimfnfcls  23224  fclscmp  23226  clssubg  23305  tgpconncompeqg  23308  tgpconncomp  23309  qustgpopn  23316  tgptsmscls  23346  xmeter  23631  metust  23759  tgqioo  24008  zcld  24021  iccntr  24029  icccmplem2  24031  icccmplem3  24032  reconnlem1  24034  reconnlem2  24035  xrge0tsms  24042  cnheiborlem  24162  om1addcl  24241  pi1blem  24247  pi1grplem  24257  pi1inv  24260  pi1xfr  24263  pi1xfrcnvlem  24264  pi1coghm  24269  cmetcaulem  24497  ivthlem2  24661  ivthlem3  24662  ovolicc2lem2  24727  ovolicc2lem5  24730  opnmbllem  24810  volcn  24815  ismbf3d  24863  mbfi1fseqlem6  24930  itg2const2  24951  i1fibl  25017  ibladd  25030  bddiblnc  25051  ditgsplitlem  25069  dvferm1lem  25193  dvferm2lem  25195  dvlip2  25204  dvivthlem1  25217  dvne0  25220  lhop1lem  25222  lhop1  25223  lhop  25225  dvcnvrelem1  25226  dvcnvrelem2  25227  dvcnvre  25228  ftc1lem1  25244  itgsubst  25258  aaliou3lem2  25548  psercnlem2  25628  efif1olem2  25744  logtayl  25860  log2tlbnd  26140  xrlimcnp  26163  pntibndlem2  26784  pntlemj  26796  pntleml  26804  trgcgr  26922  hlid  27015  hltr  27016  btwnhl1  27018  btwnhl2  27019  hlcgrex  27022  mirhl  27085  mirbtwnhl  27086  mirhl2  27087  hlpasch  27162  lnopp2hpgb  27169  cgrahl  27233  axlowdim  27374  uhgrissubgr  27687  egrsubgr  27689  uhgrspansubgr  27703  uhgrspan1  27715  cusgrrusgr  27993  wlkonwlk  28075  wlkonwlk1l  28076  wlkres  28083  wlkp1  28094  wlkd  28099  lfgriswlk  28101  wwlksnextinj  28309  2wlkond  28347  wpthswwlks2on  28371  0wlkon  28529  1wlkd  28550  1pthond  28553  eliccelico  31143  elicoelioo  31144  xrge0tsmsd  31362  tpr2rico  31907  measinb  32234  cntmeas  32239  dya2icoseg  32289  sibf0  32346  sibfof  32352  pfxwlk  33130  revwlk  33131  resconn  33253  cvmsss2  33281  cvmliftlem10  33301  mrsubco  33528  bday0b  34069  madebdaylemlrcut  34124  cofcut1  34135  cgrextend  34355  cgr3rflx  34401  cgrxfr  34402  btwnconn1lem4  34437  btwnconn1lem8  34441  btwnconn1lem11  34444  bj-pinftynminfty  35442  bj-rveccmod  35517  iooelexlt  35577  opnmbllem0  35857  ibladdnc  35878  ftc1anc  35902  isbnd3  35986  prdsbnd  35995  rngomndo  36137  isgrpda  36157  rngohomco  36176  rngoisocnv  36183  rngoidl  36226  0idl  36227  intidl  36231  unichnidl  36233  keridl  36234  smprngopr  36254  lshpnel2N  37041  lkrshp  37161  4atexlemex2  38127  4atex  38132  cdleme0moN  38281  istendod  38818  dihlspsnat  39389  dochsatshp  39507  mon1psubm  41069  iocinico  41081  dfrtrcl3  41379  eliood  43085  eliccd  43091  eliocd  43094  limciccioolb  43211  limcicciooub  43227  icccncfext  43477  iblspltprt  43563  itgspltprt  43569  fourierdlem1  43698  fourierdlem4  43701  fourierdlem32  43729  fourierdlem33  43730  fourierdlem43  43740  fourierdlem65  43761  fourierdlem79  43775  prsal  43908  issald  43921  iccpartrn  44940  fpprwpprb  45250  bgoldbtbnd  45319  expnegico01  45917  dignnld  46007  reorelicc  46114