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  8428  canthwelem  10565  intwun  10650  tskwun  10699  gruwun  10728  ixxss1  13283  ixxss2  13284  ixxss12  13285  ixxub  13286  ixxlb  13287  elicod  13315  ubioc1  13319  lbico1  13320  lbicc2  13384  ubicc2  13385  difreicc  13404  supicc  13421  modelico  13805  zmodfz  13817  addmodid  13846  dfrtrcl2  14989  phicl2  16699  4sqlem12  16888  isfuncd  17793  idfucl  17809  cofucl  17816  invfuc  17905  cnvps  18505  psss  18507  issubmd  18735  mndissubm  18736  submid  18739  subsubm  18745  0subm  18746  mhmima  18754  mhmeql  18755  gsumwspan  18775  frmdsssubm  18790  sursubmefmnd  18825  injsubmefmnd  18826  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  20326  cntzsubrng  20504  subrgsubm  20522  subrgugrp  20528  subrgint  20532  cntzsubr  20543  issubdrg  20717  lsssubg  20912  islmhm2  20994  pj1lmhm  21056  islbs2  21113  islbs3  21114  lbsextlem4  21120  issubrgd  21145  lidlsubg  21182  2idlcpblrng  21230  isphld  21613  mplsubglem  21958  mplsubrg  21964  mplind  22029  mhpsubg  22100  dmatsgrp  22447  dmatsrng  22449  scmatsgrp  22467  scmatsrng  22468  scmatsgrp1  22470  scmatsrng1  22471  cpmatsubgpmat  22668  cpmatsrgpmat  22669  lmcnp  23252  isufil2  23856  ufileu  23867  filufint  23868  fmfnfm  23906  flimclslem  23932  fclsfnflim  23975  flimfnfcls  23976  fclscmp  23978  clssubg  24057  tgpconncompeqg  24060  tgpconncomp  24061  qustgpopn  24068  tgptsmscls  24098  xmeter  24381  metust  24506  tgqioo  24748  zcld  24762  iccntr  24770  icccmplem2  24772  icccmplem3  24773  reconnlem1  24775  reconnlem2  24776  xrge0tsms  24783  cnheiborlem  24913  om1addcl  24993  pi1blem  24999  pi1grplem  25009  pi1inv  25012  pi1xfr  25015  pi1xfrcnvlem  25016  pi1coghm  25021  cmetcaulem  25248  ivthlem2  25413  ivthlem3  25414  ovolicc2lem2  25479  ovolicc2lem5  25482  opnmbllem  25562  volcn  25567  ismbf3d  25615  mbfi1fseqlem6  25681  itg2const2  25702  i1fibl  25769  ibladd  25782  bddiblnc  25803  ditgsplitlem  25821  dvferm1lem  25948  dvferm2lem  25950  dvlip2  25960  dvivthlem1  25973  dvne0  25976  lhop1lem  25978  lhop1  25979  lhop  25981  dvcnvrelem1  25982  dvcnvrelem2  25983  dvcnvre  25984  ftc1lem1  26002  itgsubst  26016  aaliou3lem2  26311  psercnlem2  26394  efif1olem2  26512  logtayl  26629  log2tlbnd  26915  xrlimcnp  26938  pntibndlem2  27562  pntlemj  27574  pntleml  27582  bday0b  27811  cuteq0  27813  cuteq1  27815  madebdaylemlrcut  27881  cofcut1  27902  onscutlt  28245  trgcgr  28571  hlid  28664  hltr  28665  btwnhl1  28667  btwnhl2  28668  hlcgrex  28671  mirhl  28734  mirbtwnhl  28735  mirhl2  28736  hlpasch  28811  lnopp2hpgb  28818  cgrahl  28882  axlowdim  29017  uhgrissubgr  29331  egrsubgr  29333  uhgrspansubgr  29347  uhgrspan1  29359  cusgrrusgr  29638  wlkonwlk  29717  wlkonwlk1l  29718  wlkres  29725  wlkp1  29736  wlkd  29741  lfgriswlk  29743  wwlksnextinj  29955  2wlkond  29993  wpthswwlks2on  30020  0wlkon  30178  1wlkd  30199  1pthond  30202  eliccelico  32838  elicoelioo  32839  xrge0tsmsd  33136  tpr2rico  34050  measinb  34359  cntmeas  34364  dya2icoseg  34415  sibf0  34472  sibfof  34478  pfxwlk  35299  revwlk  35300  resconn  35421  cvmsss2  35449  cvmliftlem10  35469  mrsubco  35696  cgrextend  36183  cgr3rflx  36229  cgrxfr  36230  btwnconn1lem4  36265  btwnconn1lem8  36269  btwnconn1lem11  36272  bj-pinftynminfty  37403  bj-rveccmod  37478  iooelexlt  37538  opnmbllem0  37828  ibladdnc  37849  ftc1anc  37873  isbnd3  37956  prdsbnd  37965  rngomndo  38107  isgrpda  38127  rngohomco  38146  rngoisocnv  38153  rngoidl  38196  0idl  38197  intidl  38201  unichnidl  38203  keridl  38204  smprngopr  38224  lshpnel2N  39282  lkrshp  39402  4atexlemex2  40368  4atex  40373  cdleme0moN  40522  istendod  41059  dihlspsnat  41630  dochsatshp  41748  mon1psubm  43477  iocinico  43490  dfrtrcl3  44010  eliood  45780  eliccd  45786  eliocd  45789  limciccioolb  45903  limcicciooub  45917  icccncfext  46167  iblspltprt  46253  itgspltprt  46259  fourierdlem1  46388  fourierdlem4  46391  fourierdlem32  46419  fourierdlem33  46420  fourierdlem43  46430  fourierdlem65  46451  fourierdlem79  46465  prsal  46598  issald  46613  iccpartrn  47712  fpprwpprb  48022  bgoldbtbnd  48091  upgrimwlk  48184  upgrimpths  48191  gpgedgvtx0  48343  gpgedgvtx1  48344  gpgprismgr4cycllem11  48387  expnegico01  48800  dignnld  48885  reorelicc  48992