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  8434  canthwelem  10573  intwun  10658  tskwun  10707  gruwun  10736  ixxss1  13316  ixxss2  13317  ixxss12  13318  ixxub  13319  ixxlb  13320  elicod  13348  ubioc1  13352  lbico1  13353  lbicc2  13417  ubicc2  13418  difreicc  13437  supicc  13454  nnge2recico01  13460  modelico  13840  zmodfz  13852  addmodid  13881  dfrtrcl2  15024  phicl2  16738  4sqlem12  16927  isfuncd  17832  idfucl  17848  cofucl  17855  invfuc  17944  cnvps  18544  psss  18546  issubmd  18774  mndissubm  18775  submid  18778  subsubm  18784  0subm  18785  mhmima  18793  mhmeql  18794  gsumwspan  18814  frmdsssubm  18829  sursubmefmnd  18864  injsubmefmnd  18865  issubgrpd2  19118  grpissubg  19122  subgint  19126  nmzsubg  19140  eqger  19153  eqgcpbl  19157  cycsubm  19177  cycsubgcl  19181  ghmrn  19204  ghmpreima  19213  gastacl  19284  cntzsubm  19313  sylow2blem1  19595  lsmsubm  19628  torsubg  19829  oddvdssubg  19830  dmdprdd  19976  dprdsubg  20001  dprdres  20005  unitsubm  20366  cntzsubrng  20544  subrgsubm  20562  subrgugrp  20568  subrgint  20572  cntzsubr  20583  issubdrg  20757  lsssubg  20952  islmhm2  21033  pj1lmhm  21095  islbs2  21152  islbs3  21153  lbsextlem4  21159  issubrgd  21184  lidlsubg  21221  2idlcpblrng  21269  isphld  21634  mplsubglem  21977  mplsubrg  21983  mplind  22048  mhpsubg  22119  dmatsgrp  22464  dmatsrng  22466  scmatsgrp  22484  scmatsrng  22485  scmatsgrp1  22487  scmatsrng1  22488  cpmatsubgpmat  22685  cpmatsrgpmat  22686  lmcnp  23269  isufil2  23873  ufileu  23884  filufint  23885  fmfnfm  23923  flimclslem  23949  fclsfnflim  23992  flimfnfcls  23993  fclscmp  23995  clssubg  24074  tgpconncompeqg  24077  tgpconncomp  24078  qustgpopn  24085  tgptsmscls  24115  xmeter  24398  metust  24523  tgqioo  24765  zcld  24779  iccntr  24787  icccmplem2  24789  icccmplem3  24790  reconnlem1  24792  reconnlem2  24793  xrge0tsms  24800  cnheiborlem  24921  om1addcl  25000  pi1blem  25006  pi1grplem  25016  pi1inv  25019  pi1xfr  25022  pi1xfrcnvlem  25023  pi1coghm  25028  cmetcaulem  25255  ivthlem2  25419  ivthlem3  25420  ovolicc2lem2  25485  ovolicc2lem5  25488  opnmbllem  25568  volcn  25573  ismbf3d  25621  mbfi1fseqlem6  25687  itg2const2  25708  i1fibl  25775  ibladd  25788  bddiblnc  25809  ditgsplitlem  25827  dvferm1lem  25951  dvferm2lem  25953  dvlip2  25962  dvivthlem1  25975  dvne0  25978  lhop1lem  25980  lhop1  25981  lhop  25983  dvcnvrelem1  25984  dvcnvrelem2  25985  dvcnvre  25986  ftc1lem1  26002  itgsubst  26016  aaliou3lem2  26309  psercnlem2  26389  efif1olem2  26507  logtayl  26624  log2tlbnd  26909  xrlimcnp  26932  pntibndlem2  27554  pntlemj  27566  pntleml  27574  bday0b  27805  cuteq0  27807  cuteq1  27809  madebdaylemlrcut  27891  cofcut1  27912  oncutlt  28256  trgcgr  28584  hlid  28677  hltr  28678  btwnhl1  28680  btwnhl2  28681  hlcgrex  28684  mirhl  28747  mirbtwnhl  28748  mirhl2  28749  hlpasch  28824  lnopp2hpgb  28831  cgrahl  28895  axlowdim  29030  uhgrissubgr  29344  egrsubgr  29346  uhgrspansubgr  29360  uhgrspan1  29372  cusgrrusgr  29650  wlkonwlk  29729  wlkonwlk1l  29730  wlkres  29737  wlkp1  29748  wlkd  29753  lfgriswlk  29755  wwlksnextinj  29967  2wlkond  30005  wpthswwlks2on  30032  0wlkon  30190  1wlkd  30211  1pthond  30214  eliccelico  32850  elicoelioo  32851  xrge0tsmsd  33134  tpr2rico  34056  measinb  34365  cntmeas  34370  dya2icoseg  34421  sibf0  34478  sibfof  34484  pfxwlk  35306  revwlk  35307  resconn  35428  cvmsss2  35456  cvmliftlem10  35476  mrsubco  35703  cgrextend  36190  cgr3rflx  36236  cgrxfr  36237  btwnconn1lem4  36272  btwnconn1lem8  36276  btwnconn1lem11  36279  bj-pinftynminfty  37541  bj-rveccmod  37616  iooelexlt  37678  opnmbllem0  37977  ibladdnc  37998  ftc1anc  38022  isbnd3  38105  prdsbnd  38114  rngomndo  38256  isgrpda  38276  rngohomco  38295  rngoisocnv  38302  rngoidl  38345  0idl  38346  intidl  38350  unichnidl  38352  keridl  38353  smprngopr  38373  lshpnel2N  39431  lkrshp  39551  4atexlemex2  40517  4atex  40522  cdleme0moN  40671  istendod  41208  dihlspsnat  41779  dochsatshp  41897  mon1psubm  43627  iocinico  43640  dfrtrcl3  44160  eliood  45928  eliccd  45934  eliocd  45937  limciccioolb  46051  limcicciooub  46065  icccncfext  46315  iblspltprt  46401  itgspltprt  46407  fourierdlem1  46536  fourierdlem4  46539  fourierdlem32  46567  fourierdlem33  46568  fourierdlem43  46578  fourierdlem65  46599  fourierdlem79  46613  prsal  46746  issald  46761  flmrecm1  47785  iccpartrn  47884  fpprwpprb  48210  bgoldbtbnd  48279  upgrimwlk  48372  upgrimpths  48379  gpgedgvtx0  48531  gpgedgvtx1  48532  gpgprismgr4cycllem11  48575  expnegico01  48988  dignnld  49073  reorelicc  49180