Theorem mpbir3and 1338

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

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

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 399  df-3an 1085

This theorem is referenced by:  canthwelem  10074  intwun  10159  tskwun  10208  gruwun  10237  ixxss1  12759  ixxss2  12760  ixxss12  12761  ixxub  12762  ixxlb  12763  elicod  12790  ubioc1  12793  lbico1  12794  lbicc2  12855  ubicc2  12856  difreicc  12873  supicc  12889  modelico  13252  zmodfz  13264  addmodid  13290  dfrtrcl2  14423  phicl2  16107  4sqlem12  16294  isfuncd  17137  idfucl  17153  cofucl  17160  invfuc  17246  cnvps  17824  psss  17826  issubmd  17973  mndissubm  17974  submid  17977  subsubm  17983  0subm  17984  mhmima  17991  mhmeql  17992  gsumwspan  18013  frmdsssubm  18028  sursubmefmnd  18063  injsubmefmnd  18064  issubgrpd2  18297  grpissubg  18301  subgint  18305  0subg  18306  nmzsubg  18319  eqger  18332  eqgcpbl  18336  cycsubm  18347  cycsubgcl  18351  ghmrn  18373  ghmpreima  18382  gastacl  18441  cntzsubm  18468  sylow2blem1  18747  lsmsubm  18780  torsubg  18976  oddvdssubg  18977  dmdprdd  19123  dprdsubg  19148  dprdres  19152  unitsubm  19422  subrgsubm  19550  subrgugrp  19556  subrgint  19559  issubdrg  19562  cntzsubr  19570  lsssubg  19731  islmhm2  19812  pj1lmhm  19874  islbs2  19928  islbs3  19929  lbsextlem4  19935  issubrngd2  19963  lidlsubg  19990  2idlcpbl  20009  mplsubglem  20216  mplsubrg  20222  mplind  20284  mhpsubg  20342  isphld  20800  dmatsgrp  21110  dmatsrng  21112  scmatsgrp  21130  scmatsrng  21131  scmatsgrp1  21133  scmatsrng1  21134  cpmatsubgpmat  21330  cpmatsrgpmat  21331  lmcnp  21914  isufil2  22518  ufileu  22529  filufint  22530  fmfnfm  22568  flimclslem  22594  fclsfnflim  22637  flimfnfcls  22638  fclscmp  22640  clssubg  22719  tgpconncompeqg  22722  tgpconncomp  22723  qustgpopn  22730  tgptsmscls  22760  xmeter  23045  metust  23170  tgqioo  23410  zcld  23423  iccntr  23431  icccmplem2  23433  icccmplem3  23434  reconnlem1  23436  reconnlem2  23437  xrge0tsms  23444  cnheiborlem  23560  om1addcl  23639  pi1blem  23645  pi1grplem  23655  pi1inv  23658  pi1xfr  23661  pi1xfrcnvlem  23662  pi1coghm  23667  cmetcaulem  23893  ivthlem2  24055  ivthlem3  24056  ovolicc2lem2  24121  ovolicc2lem5  24124  opnmbllem  24204  volcn  24209  ismbf3d  24257  mbfi1fseqlem6  24323  itg2const2  24344  i1fibl  24410  ibladd  24423  ditgsplitlem  24460  dvferm1lem  24583  dvferm2lem  24585  dvlip2  24594  dvivthlem1  24607  dvne0  24610  lhop1lem  24612  lhop1  24613  lhop  24615  dvcnvrelem1  24616  dvcnvrelem2  24617  dvcnvre  24618  ftc1lem1  24634  itgsubst  24648  aaliou3lem2  24934  psercnlem2  25014  efif1olem2  25129  logtayl  25245  log2tlbnd  25525  xrlimcnp  25548  pntibndlem2  26169  pntlemj  26181  pntleml  26189  trgcgr  26304  hlid  26397  hltr  26398  btwnhl1  26400  btwnhl2  26401  hlcgrex  26404  mirhl  26467  mirbtwnhl  26468  mirhl2  26469  hlpasch  26544  lnopp2hpgb  26551  cgrahl  26615  axlowdim  26749  uhgrissubgr  27059  egrsubgr  27061  uhgrspansubgr  27075  uhgrspan1  27087  cusgrrusgr  27365  wlkonwlk  27446  wlkonwlk1l  27447  wlkres  27454  wlkp1  27465  wlkd  27470  lfgriswlk  27472  wwlksnextinj  27679  2wlkond  27718  wpthswwlks2on  27742  0wlkon  27901  1wlkd  27922  1pthond  27925  eliccelico  30502  elicoelioo  30503  xrge0tsmsd  30694  tpr2rico  31157  measinb  31482  cntmeas  31487  dya2icoseg  31537  sibf0  31594  sibfof  31600  pfxwlk  32372  revwlk  32373  resconn  32495  cvmsss2  32523  cvmliftlem10  32543  mrsubco  32770  cgrextend  33471  cgr3rflx  33517  cgrxfr  33518  btwnconn1lem4  33553  btwnconn1lem8  33557  btwnconn1lem11  33560  bj-pinftynminfty  34511  bj-rveccmod  34585  iooelexlt  34645  opnmbllem0  34930  ibladdnc  34951  bddiblnc  34964  ftc1anc  34977  isbnd3  35064  prdsbnd  35073  rngomndo  35215  isgrpda  35235  rngohomco  35254  rngoisocnv  35261  rngoidl  35304  0idl  35305  intidl  35309  unichnidl  35311  keridl  35312  smprngopr  35332  lshpnel2N  36123  lkrshp  36243  4atexlemex2  37209  4atex  37214  cdleme0moN  37363  istendod  37900  dihlspsnat  38471  dochsatshp  38589  mon1psubm  39813  iocinico  39825  dfrtrcl3  40085  eliood  41780  eliccd  41786  eliocd  41790  limciccioolb  41909  limcicciooub  41925  icccncfext  42177  iblspltprt  42265  itgspltprt  42271  fourierdlem1  42400  fourierdlem4  42403  fourierdlem32  42431  fourierdlem33  42432  fourierdlem43  42442  fourierdlem65  42463  fourierdlem79  42477  prsal  42610  issald  42623  iccpartrn  43597  fpprwpprb  43912  bgoldbtbnd  43981  expnegico01  44580  dignnld  44670  reorelicc  44704