Theorem mpbir3and 1357

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1099

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 209  df-an 400  df-3an 1101

This theorem is referenced by:  2ellim  8468  canthwelem  10619  intwun  10704  tskwun  10753  gruwun  10782  ixxss1  13377  ixxss2  13378  ixxss12  13379  ixxub  13380  ixxlb  13381  elicod  13409  ubioc1  13413  lbico1  13414  lbicc2  13478  ubicc2  13479  difreicc  13498  supicc  13515  nnge2recico01  13521  modelico  13901  zmodfz  13913  addmodid  13942  dfrtrcl2  15085  phicl2  16813  4sqlem12  17002  isfuncd  17908  idfucl  17924  cofucl  17931  invfuc  18020  cnvps  18620  psss  18622  issubmd  18850  mndissubm  18851  submid  18854  subsubm  18860  0subm  18861  mhmima  18869  mhmeql  18870  gsumwspan  18890  frmdsssubm  18905  sursubmefmnd  18940  injsubmefmnd  18941  issubgrpd2  19194  grpissubg  19198  subgint  19202  nmzsubg  19216  eqger  19229  eqgcpbl  19233  cycsubm  19253  cycsubgcl  19257  ghmrn  19279  ghmpreima  19288  gastacl  19359  cntzsubm  19388  sylow2blem1  19670  lsmsubm  19703  torsubg  19904  oddvdssubg  19905  dmdprdd  20051  dprdsubg  20076  dprdres  20080  unitsubm  20445  cntzsubrng  20627  subrgsubm  20645  subrgugrp  20651  subrgint  20655  cntzsubr  20666  issubdrg  20836  lsssubg  21031  islmhm2  21112  pj1lmhm  21174  islbs2  21231  islbs3  21232  lbsextlem4  21238  issubrgd  21263  lidlsubg  21300  2idlcpblrng  21348  isphld  21713  mplsubglem  22057  mplsubrg  22063  mplind  22130  mhpsubg  22225  dmatsgrp  22566  dmatsrng  22568  scmatsgrp  22586  scmatsrng  22587  scmatsgrp1  22589  scmatsrng1  22590  cpmatsubgpmat  22787  cpmatsrgpmat  22788  lmcnp  23371  isufil2  23975  ufileu  23986  filufint  23987  fmfnfm  24025  flimclslem  24051  fclsfnflim  24094  flimfnfcls  24095  fclscmp  24097  clssubg  24176  tgpconncompeqg  24179  tgpconncomp  24180  qustgpopn  24187  tgptsmscls  24217  xmeter  24500  metust  24625  tgqioo  24867  zcld  24881  iccntr  24889  icccmplem2  24891  icccmplem3  24892  reconnlem1  24894  reconnlem2  24895  xrge0tsms  24902  cnheiborlem  25023  om1addcl  25102  pi1blem  25108  pi1grplem  25118  pi1inv  25121  pi1xfr  25124  pi1xfrcnvlem  25125  pi1coghm  25130  cmetcaulem  25357  ivthlem2  25521  ivthlem3  25522  ovolicc2lem2  25587  ovolicc2lem5  25590  opnmbllem  25670  volcn  25675  ismbf3d  25723  mbfi1fseqlem6  25789  itg2const2  25810  i1fibl  25877  ibladd  25890  bddiblnc  25911  ditgsplitlem  25929  dvferm1lem  26053  dvferm2lem  26055  dvlip2  26064  dvivthlem1  26077  dvne0  26080  lhop1lem  26082  lhop1  26083  lhop  26085  dvcnvrelem1  26086  dvcnvrelem2  26087  dvcnvre  26088  ftc1lem1  26104  itgsubst  26118  aaliou3lem2  26414  psercnlem2  26494  efif1olem2  26615  logtayl  26732  log2tlbnd  27017  xrlimcnp  27040  pntibndlem2  27662  pntlemj  27674  pntleml  27682  bday0b  27913  cuteq0  27915  cuteq1  27917  madebdaylemlrcut  27999  cofcut1  28020  oncutlt  28364  trgcgr  28692  hlid  28785  hltr  28786  btwnhl1  28788  btwnhl2  28789  hlcgrex  28792  mirhl  28859  mirbtwnhl  28860  mirhl2  28861  hlpasch  28936  lnopp2hpgb  28943  cgrahl  29028  axlowdim  29169  uhgrissubgr  29483  egrsubgr  29485  uhgrspansubgr  29499  uhgrspan1  29511  cusgrrusgr  29789  wlkonwlk  29868  wlkonwlk1l  29869  wlkres  29876  wlkp1  29887  wlkd  29892  lfgriswlk  29894  wwlksnextinj  30106  2wlkond  30144  wpthswwlks2on  30171  0wlkon  30329  1wlkd  30350  1pthond  30353  eliccelico  32985  elicoelioo  32986  xrge0tsmsd  33259  tpr2rico  34211  measinb  34520  cntmeas  34525  dya2icoseg  34576  sibf0  34633  sibfof  34639  pfxwlk  35479  revwlk  35480  resconn  35601  cvmsss2  35629  cvmliftlem10  35649  mrsubco  35876  cgrextend  36363  cgr3rflx  36409  cgrxfr  36410  btwnconn1lem4  36445  btwnconn1lem8  36449  btwnconn1lem11  36452  bj-pinftynminfty  37724  bj-rveccmod  37799  iooelexlt  37861  opnmbllem0  38160  ibladdnc  38181  ftc1anc  38205  isbnd3  38288  prdsbnd  38297  rngomndo  38439  isgrpda  38459  rngohomco  38478  rngoisocnv  38485  rngoidl  38528  0idl  38529  intidl  38533  unichnidl  38535  keridl  38536  smprngopr  38556  lshpnel2N  39614  lkrshp  39734  4atexlemex2  40700  4atex  40705  cdleme0moN  40854  istendod  41391  dihlspsnat  41962  dochsatshp  42080  mon1psubm  43781  iocinico  43794  dfrtrcl3  44314  eliood  46065  eliccd  46071  eliocd  46074  limciccioolb  46188  limcicciooub  46202  icccncfext  46452  iblspltprt  46538  itgspltprt  46544  fourierdlem1  46673  fourierdlem4  46676  fourierdlem32  46704  fourierdlem33  46705  fourierdlem43  46715  fourierdlem65  46736  fourierdlem79  46750  prsal  46883  issald  46898  flmrecm1  47928  iccpartrn  48027  fpprwpprb  48353  bgoldbtbnd  48422  upgrimwlk  48515  upgrimpths  48522  gpgedgvtx0  48674  gpgedgvtx1  48675  gpgprismgr4cycllem11  48718  expnegico01  49131  dignnld  49216  reorelicc  49323