Theorem mpbir3and 1361

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1105

This theorem is used by:  2ellim  8480  canthwelem  10639  intwun  10724  tskwun  10773  gruwun  10802  ixxss1  13394  ixxss2  13395  ixxss12  13396  ixxub  13397  ixxlb  13398  elicod  13426  ubioc1  13430  lbico1  13431  lbicc2  13495  ubicc2  13496  difreicc  13515  supicc  13532  nnge2recico01  13538  modelico  13919  zmodfz  13931  addmodid  13960  dfrtrcl2  15104  phicl2  16831  4sqlem12  17020  isfuncd  17926  idfucl  17942  cofucl  17949  invfuc  18038  cnvps  18638  psss  18640  issubmd  18868  mndissubm  18869  submid  18872  subsubm  18879  0subm  18880  mhmima  18888  mhmeql  18889  gsumwspan  18909  frmdsssubm  18924  sursubmefmnd  18959  injsubmefmnd  18960  issubgrpd2  19213  grpissubg  19217  subgint  19221  nmzsubg  19235  eqger  19250  eqgcpbl  19254  cycsubm  19277  cycsubgcl  19281  ghmrn  19303  ghmpreima  19312  gastacl  19383  cntzsubm  19412  sylow2blem1  19694  lsmsubm  19727  torsubg  19928  oddvdssubg  19929  dmdprdd  20075  dprdsubg  20100  dprdres  20104  unitsubm  20473  cntzsubrng  20675  subrgsubm  20693  subrgugrp  20699  subrgint  20703  cntzsubr  20714  issubdrg  20892  lsssubg  21087  islmhm2  21168  pj1lmhm  21230  islbs2  21287  islbs3  21288  lbsextlem4  21294  issubrgd  21319  lidlsubg  21357  2idlcpblrng  21419  isphld  21813  mplsubglem  22157  mplsubrg  22163  mplind  22230  mhpsubg  22325  dmatsgrp  22665  dmatsrng  22667  scmatsgrp  22685  scmatsrng  22686  scmatsgrp1  22688  scmatsrng1  22689  cpmatsubgpmat  22886  cpmatsrgpmat  22887  lmcnp  23470  isufil2  24074  ufileu  24085  filufint  24086  fmfnfm  24124  flimclslem  24150  fclsfnflim  24193  flimfnfcls  24194  fclscmp  24196  clssubg  24275  tgpconncompeqg  24278  tgpconncomp  24279  qustgpopn  24286  tgptsmscls  24316  xmeter  24599  metust  24724  tgqioo  24966  zcld  24980  iccntr  24988  icccmplem2  24990  icccmplem3  24991  reconnlem1  24993  reconnlem2  24994  xrge0tsms  25001  cnheiborlem  25122  om1addcl  25201  pi1blem  25207  pi1grplem  25217  pi1inv  25220  pi1xfr  25223  pi1xfrcnvlem  25224  pi1coghm  25229  cmetcaulem  25456  ivthlem2  25620  ivthlem3  25621  ovolicc2lem2  25686  ovolicc2lem5  25689  opnmbllem  25769  volcn  25774  ismbf3d  25822  mbfi1fseqlem6  25888  itg2const2  25909  i1fibl  25976  ibladd  25989  bddiblnc  26010  ditgsplitlem  26028  dvferm1lem  26152  dvferm2lem  26154  dvlip2  26163  dvivthlem1  26176  dvne0  26179  lhop1lem  26181  lhop1  26182  lhop  26184  dvcnvrelem1  26185  dvcnvrelem2  26186  dvcnvre  26187  ftc1lem1  26203  itgsubst  26217  aaliou3lem2  26515  psercnlem2  26596  efif1olem2  26717  logtayl  26834  log2tlbnd  27119  xrlimcnp  27142  pntibndlem2  27764  pntlemj  27776  pntleml  27784  bday0b  28015  cuteq0  28017  cuteq1  28019  madebdaylemlrcut  28101  cofcut1  28122  oncutlt  28466  trgcgr  28794  hlid  28890  hltr  28891  btwnhl1  28893  btwnhl2  28894  hlcgrex  28897  mirhl  28965  mirbtwnhl  28966  mirhl2  28967  hlpasch  29047  lnopp2hpgb  29054  cgrahl  29147  axlowdim  29320  uhgrissubgr  29634  egrsubgr  29636  uhgrspansubgr  29650  uhgrspan1  29662  cusgrrusgr  29940  wlkonwlk  30019  wlkonwlk1l  30020  wlkres  30027  wlkp1  30038  wlkd  30043  lfgriswlk  30045  wwlksnextinj  30257  2wlkond  30295  wpthswwlks2on  30322  0wlkon  30480  1wlkd  30501  1pthond  30504  eliccelico  33131  elicoelioo  33132  xrge0tsmsd  33402  tpr2rico  34311  measinb  34620  cntmeas  34625  dya2icoseg  34676  sibf0  34733  sibfof  34739  pfxwlk  35624  revwlk  35625  resconn  35746  cvmsss2  35774  cvmliftlem10  35794  mrsubco  36021  cgrextend  36508  cgr3rflx  36554  cgrxfr  36555  btwnconn1lem4  36590  btwnconn1lem8  36594  btwnconn1lem11  36597  bj-pinftynminfty  37899  bj-rveccmod  37974  iooelexlt  38036  opnmbllem0  38335  ibladdnc  38356  ftc1anc  38380  isbnd3  38463  prdsbnd  38472  rngomndo  38614  isgrpda  38634  rngohomco  38653  rngoisocnv  38660  rngoidl  38703  0idl  38704  intidl  38708  unichnidl  38710  keridl  38711  smprngopr  38731  lshpnel2N  39787  lkrshp  39907  4atexlemex2  40873  4atex  40878  cdleme0moN  41027  istendod  41564  dihlspsnat  42135  dochsatshp  42253  mon1psubm  43954  iocinico  43967  dfrtrcl3  44487  eliood  46242  eliccd  46248  eliocd  46251  limciccioolb  46365  limcicciooub  46379  icccncfext  46629  iblspltprt  46715  itgspltprt  46721  fourierdlem1  46850  fourierdlem4  46853  fourierdlem32  46881  fourierdlem33  46882  fourierdlem43  46892  fourierdlem65  46913  fourierdlem79  46927  prsal  47060  issald  47075  flmrecm1  48108  iccpartrn  48207  fpprwpprb  48533  bgoldbtbnd  48602  upgrimwlk  48695  upgrimpths  48702  gpgedgvtx0  48854  gpgedgvtx1  48855  gpgprismgr4cycllem11  48898  smprngprmrng  49132  expnegico01  49326  dignnld  49411  reorelicc  49518