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  8429  canthwelem  10566  intwun  10651  tskwun  10700  gruwun  10729  ixxss1  13284  ixxss2  13285  ixxss12  13286  ixxub  13287  ixxlb  13288  elicod  13316  ubioc1  13320  lbico1  13321  lbicc2  13385  ubicc2  13386  difreicc  13405  supicc  13422  modelico  13806  zmodfz  13818  addmodid  13847  dfrtrcl2  14990  phicl2  16700  4sqlem12  16889  isfuncd  17794  idfucl  17810  cofucl  17817  invfuc  17906  cnvps  18506  psss  18508  issubmd  18736  mndissubm  18737  submid  18740  subsubm  18746  0subm  18747  mhmima  18755  mhmeql  18756  gsumwspan  18776  frmdsssubm  18791  sursubmefmnd  18826  injsubmefmnd  18827  issubgrpd2  19077  grpissubg  19081  subgint  19085  nmzsubg  19099  eqger  19112  eqgcpbl  19116  cycsubm  19136  cycsubgcl  19140  ghmrn  19163  ghmpreima  19172  gastacl  19243  cntzsubm  19272  sylow2blem1  19554  lsmsubm  19587  torsubg  19788  oddvdssubg  19789  dmdprdd  19935  dprdsubg  19960  dprdres  19964  unitsubm  20327  cntzsubrng  20505  subrgsubm  20523  subrgugrp  20529  subrgint  20533  cntzsubr  20544  issubdrg  20718  lsssubg  20913  islmhm2  20995  pj1lmhm  21057  islbs2  21114  islbs3  21115  lbsextlem4  21121  issubrgd  21146  lidlsubg  21183  2idlcpblrng  21231  isphld  21614  mplsubglem  21959  mplsubrg  21965  mplind  22030  mhpsubg  22101  dmatsgrp  22448  dmatsrng  22450  scmatsgrp  22468  scmatsrng  22469  scmatsgrp1  22471  scmatsrng1  22472  cpmatsubgpmat  22669  cpmatsrgpmat  22670  lmcnp  23253  isufil2  23857  ufileu  23868  filufint  23869  fmfnfm  23907  flimclslem  23933  fclsfnflim  23976  flimfnfcls  23977  fclscmp  23979  clssubg  24058  tgpconncompeqg  24061  tgpconncomp  24062  qustgpopn  24069  tgptsmscls  24099  xmeter  24382  metust  24507  tgqioo  24749  zcld  24763  iccntr  24771  icccmplem2  24773  icccmplem3  24774  reconnlem1  24776  reconnlem2  24777  xrge0tsms  24784  cnheiborlem  24914  om1addcl  24994  pi1blem  25000  pi1grplem  25010  pi1inv  25013  pi1xfr  25016  pi1xfrcnvlem  25017  pi1coghm  25022  cmetcaulem  25249  ivthlem2  25414  ivthlem3  25415  ovolicc2lem2  25480  ovolicc2lem5  25483  opnmbllem  25563  volcn  25568  ismbf3d  25616  mbfi1fseqlem6  25682  itg2const2  25703  i1fibl  25770  ibladd  25783  bddiblnc  25804  ditgsplitlem  25822  dvferm1lem  25949  dvferm2lem  25951  dvlip2  25961  dvivthlem1  25974  dvne0  25977  lhop1lem  25979  lhop1  25980  lhop  25982  dvcnvrelem1  25983  dvcnvrelem2  25984  dvcnvre  25985  ftc1lem1  26003  itgsubst  26017  aaliou3lem2  26312  psercnlem2  26395  efif1olem2  26513  logtayl  26630  log2tlbnd  26916  xrlimcnp  26939  pntibndlem2  27563  pntlemj  27575  pntleml  27583  bday0b  27814  cuteq0  27816  cuteq1  27818  madebdaylemlrcut  27900  cofcut1  27921  oncutlt  28265  trgcgr  28593  hlid  28686  hltr  28687  btwnhl1  28689  btwnhl2  28690  hlcgrex  28693  mirhl  28756  mirbtwnhl  28757  mirhl2  28758  hlpasch  28833  lnopp2hpgb  28840  cgrahl  28904  axlowdim  29039  uhgrissubgr  29353  egrsubgr  29355  uhgrspansubgr  29369  uhgrspan1  29381  cusgrrusgr  29660  wlkonwlk  29739  wlkonwlk1l  29740  wlkres  29747  wlkp1  29758  wlkd  29763  lfgriswlk  29765  wwlksnextinj  29977  2wlkond  30015  wpthswwlks2on  30042  0wlkon  30200  1wlkd  30221  1pthond  30224  eliccelico  32860  elicoelioo  32861  xrge0tsmsd  33159  tpr2rico  34082  measinb  34391  cntmeas  34396  dya2icoseg  34447  sibf0  34504  sibfof  34510  pfxwlk  35331  revwlk  35332  resconn  35453  cvmsss2  35481  cvmliftlem10  35501  mrsubco  35728  cgrextend  36215  cgr3rflx  36261  cgrxfr  36262  btwnconn1lem4  36297  btwnconn1lem8  36301  btwnconn1lem11  36304  bj-pinftynminfty  37445  bj-rveccmod  37520  iooelexlt  37580  opnmbllem0  37870  ibladdnc  37891  ftc1anc  37915  isbnd3  37998  prdsbnd  38007  rngomndo  38149  isgrpda  38169  rngohomco  38188  rngoisocnv  38195  rngoidl  38238  0idl  38239  intidl  38243  unichnidl  38245  keridl  38246  smprngopr  38266  lshpnel2N  39324  lkrshp  39444  4atexlemex2  40410  4atex  40415  cdleme0moN  40564  istendod  41101  dihlspsnat  41672  dochsatshp  41790  mon1psubm  43519  iocinico  43532  dfrtrcl3  44052  eliood  45821  eliccd  45827  eliocd  45830  limciccioolb  45944  limcicciooub  45958  icccncfext  46208  iblspltprt  46294  itgspltprt  46300  fourierdlem1  46429  fourierdlem4  46432  fourierdlem32  46460  fourierdlem33  46461  fourierdlem43  46471  fourierdlem65  46492  fourierdlem79  46506  prsal  46639  issald  46654  iccpartrn  47753  fpprwpprb  48063  bgoldbtbnd  48132  upgrimwlk  48225  upgrimpths  48232  gpgedgvtx0  48384  gpgedgvtx1  48385  gpgprismgr4cycllem11  48428  expnegico01  48841  dignnld  48926  reorelicc  49033