Theorem mpbir3and 1360

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

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

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 1104

This theorem is used by:  2ellim  8482  canthwelem  10641  intwun  10726  tskwun  10775  gruwun  10804  ixxss1  13396  ixxss2  13397  ixxss12  13398  ixxub  13399  ixxlb  13400  elicod  13428  ubioc1  13432  lbico1  13433  lbicc2  13497  ubicc2  13498  difreicc  13517  supicc  13534  nnge2recico01  13540  modelico  13921  zmodfz  13933  addmodid  13962  dfrtrcl2  15106  phicl2  16833  4sqlem12  17022  isfuncd  17928  idfucl  17944  cofucl  17951  invfuc  18040  cnvps  18640  psss  18642  issubmd  18870  mndissubm  18871  submid  18874  subsubm  18881  0subm  18882  mhmima  18890  mhmeql  18891  gsumwspan  18911  frmdsssubm  18926  sursubmefmnd  18961  injsubmefmnd  18962  issubgrpd2  19215  grpissubg  19219  subgint  19223  nmzsubg  19237  eqger  19252  eqgcpbl  19256  cycsubm  19279  cycsubgcl  19283  ghmrn  19305  ghmpreima  19314  gastacl  19385  cntzsubm  19414  sylow2blem1  19696  lsmsubm  19729  torsubg  19930  oddvdssubg  19931  dmdprdd  20077  dprdsubg  20102  dprdres  20106  unitsubm  20475  cntzsubrng  20677  subrgsubm  20695  subrgugrp  20701  subrgint  20705  cntzsubr  20716  issubdrg  20894  lsssubg  21089  islmhm2  21170  pj1lmhm  21232  islbs2  21289  islbs3  21290  lbsextlem4  21296  issubrgd  21321  lidlsubg  21359  2idlcpblrng  21421  isphld  21815  mplsubglem  22159  mplsubrg  22165  mplind  22232  mhpsubg  22327  dmatsgrp  22667  dmatsrng  22669  scmatsgrp  22687  scmatsrng  22688  scmatsgrp1  22690  scmatsrng1  22691  cpmatsubgpmat  22888  cpmatsrgpmat  22889  lmcnp  23472  isufil2  24076  ufileu  24087  filufint  24088  fmfnfm  24126  flimclslem  24152  fclsfnflim  24195  flimfnfcls  24196  fclscmp  24198  clssubg  24277  tgpconncompeqg  24280  tgpconncomp  24281  qustgpopn  24288  tgptsmscls  24318  xmeter  24601  metust  24726  tgqioo  24968  zcld  24982  iccntr  24990  icccmplem2  24992  icccmplem3  24993  reconnlem1  24995  reconnlem2  24996  xrge0tsms  25003  cnheiborlem  25124  om1addcl  25203  pi1blem  25209  pi1grplem  25219  pi1inv  25222  pi1xfr  25225  pi1xfrcnvlem  25226  pi1coghm  25231  cmetcaulem  25458  ivthlem2  25622  ivthlem3  25623  ovolicc2lem2  25688  ovolicc2lem5  25691  opnmbllem  25771  volcn  25776  ismbf3d  25824  mbfi1fseqlem6  25890  itg2const2  25911  i1fibl  25978  ibladd  25991  bddiblnc  26012  ditgsplitlem  26030  dvferm1lem  26154  dvferm2lem  26156  dvlip2  26165  dvivthlem1  26178  dvne0  26181  lhop1lem  26183  lhop1  26184  lhop  26186  dvcnvrelem1  26187  dvcnvrelem2  26188  dvcnvre  26189  ftc1lem1  26205  itgsubst  26219  aaliou3lem2  26517  psercnlem2  26598  efif1olem2  26719  logtayl  26836  log2tlbnd  27121  xrlimcnp  27144  pntibndlem2  27766  pntlemj  27778  pntleml  27786  bday0b  28017  cuteq0  28019  cuteq1  28021  madebdaylemlrcut  28103  cofcut1  28124  oncutlt  28468  trgcgr  28796  hlid  28892  hltr  28893  btwnhl1  28895  btwnhl2  28896  hlcgrex  28899  mirhl  28967  mirbtwnhl  28968  mirhl2  28969  hlpasch  29049  lnopp2hpgb  29056  cgrahl  29149  axlowdim  29322  uhgrissubgr  29636  egrsubgr  29638  uhgrspansubgr  29652  uhgrspan1  29664  cusgrrusgr  29942  wlkonwlk  30021  wlkonwlk1l  30022  wlkres  30029  wlkp1  30040  wlkd  30045  lfgriswlk  30047  wwlksnextinj  30259  2wlkond  30297  wpthswwlks2on  30324  0wlkon  30482  1wlkd  30503  1pthond  30506  eliccelico  33133  elicoelioo  33134  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