Theorem mpbir3and 1343

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086

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 1088

This theorem is referenced by:  2ellim  8420  canthwelem  10547  intwun  10632  tskwun  10681  gruwun  10710  ixxss1  13269  ixxss2  13270  ixxss12  13271  ixxub  13272  ixxlb  13273  elicod  13301  ubioc1  13305  lbico1  13306  lbicc2  13370  ubicc2  13371  difreicc  13390  supicc  13407  modelico  13791  zmodfz  13803  addmodid  13832  dfrtrcl2  14975  phicl2  16685  4sqlem12  16874  isfuncd  17778  idfucl  17794  cofucl  17801  invfuc  17890  cnvps  18490  psss  18492  issubmd  18720  mndissubm  18721  submid  18724  subsubm  18730  0subm  18731  mhmima  18739  mhmeql  18740  gsumwspan  18760  frmdsssubm  18775  sursubmefmnd  18810  injsubmefmnd  18811  issubgrpd2  19061  grpissubg  19065  subgint  19069  nmzsubg  19083  eqger  19096  eqgcpbl  19100  cycsubm  19120  cycsubgcl  19124  ghmrn  19147  ghmpreima  19156  gastacl  19227  cntzsubm  19256  sylow2blem1  19538  lsmsubm  19571  torsubg  19772  oddvdssubg  19773  dmdprdd  19919  dprdsubg  19944  dprdres  19948  unitsubm  20310  cntzsubrng  20488  subrgsubm  20506  subrgugrp  20512  subrgint  20516  cntzsubr  20527  issubdrg  20701  lsssubg  20896  islmhm2  20978  pj1lmhm  21040  islbs2  21097  islbs3  21098  lbsextlem4  21104  issubrgd  21129  lidlsubg  21166  2idlcpblrng  21214  isphld  21597  mplsubglem  21942  mplsubrg  21948  mplind  22011  mhpsubg  22074  dmatsgrp  22420  dmatsrng  22422  scmatsgrp  22440  scmatsrng  22441  scmatsgrp1  22443  scmatsrng1  22444  cpmatsubgpmat  22641  cpmatsrgpmat  22642  lmcnp  23225  isufil2  23829  ufileu  23840  filufint  23841  fmfnfm  23879  flimclslem  23905  fclsfnflim  23948  flimfnfcls  23949  fclscmp  23951  clssubg  24030  tgpconncompeqg  24033  tgpconncomp  24034  qustgpopn  24041  tgptsmscls  24071  xmeter  24354  metust  24479  tgqioo  24721  zcld  24735  iccntr  24743  icccmplem2  24745  icccmplem3  24746  reconnlem1  24748  reconnlem2  24749  xrge0tsms  24756  cnheiborlem  24886  om1addcl  24966  pi1blem  24972  pi1grplem  24982  pi1inv  24985  pi1xfr  24988  pi1xfrcnvlem  24989  pi1coghm  24994  cmetcaulem  25221  ivthlem2  25386  ivthlem3  25387  ovolicc2lem2  25452  ovolicc2lem5  25455  opnmbllem  25535  volcn  25540  ismbf3d  25588  mbfi1fseqlem6  25654  itg2const2  25675  i1fibl  25742  ibladd  25755  bddiblnc  25776  ditgsplitlem  25794  dvferm1lem  25921  dvferm2lem  25923  dvlip2  25933  dvivthlem1  25946  dvne0  25949  lhop1lem  25951  lhop1  25952  lhop  25954  dvcnvrelem1  25955  dvcnvrelem2  25956  dvcnvre  25957  ftc1lem1  25975  itgsubst  25989  aaliou3lem2  26284  psercnlem2  26367  efif1olem2  26485  logtayl  26602  log2tlbnd  26888  xrlimcnp  26911  pntibndlem2  27535  pntlemj  27547  pntleml  27555  bday0b  27780  cuteq0  27782  cuteq1  27784  madebdaylemlrcut  27850  cofcut1  27870  onscutlt  28207  trgcgr  28500  hlid  28593  hltr  28594  btwnhl1  28596  btwnhl2  28597  hlcgrex  28600  mirhl  28663  mirbtwnhl  28664  mirhl2  28665  hlpasch  28740  lnopp2hpgb  28747  cgrahl  28811  axlowdim  28946  uhgrissubgr  29260  egrsubgr  29262  uhgrspansubgr  29276  uhgrspan1  29288  cusgrrusgr  29567  wlkonwlk  29646  wlkonwlk1l  29647  wlkres  29654  wlkp1  29665  wlkd  29670  lfgriswlk  29672  wwlksnextinj  29884  2wlkond  29922  wpthswwlks2on  29949  0wlkon  30107  1wlkd  30128  1pthond  30131  eliccelico  32767  elicoelioo  32768  xrge0tsmsd  33049  tpr2rico  33932  measinb  34241  cntmeas  34246  dya2icoseg  34297  sibf0  34354  sibfof  34360  pfxwlk  35175  revwlk  35176  resconn  35297  cvmsss2  35325  cvmliftlem10  35345  mrsubco  35572  cgrextend  36059  cgr3rflx  36105  cgrxfr  36106  btwnconn1lem4  36141  btwnconn1lem8  36145  btwnconn1lem11  36148  bj-pinftynminfty  37278  bj-rveccmod  37353  iooelexlt  37413  opnmbllem0  37702  ibladdnc  37723  ftc1anc  37747  isbnd3  37830  prdsbnd  37839  rngomndo  37981  isgrpda  38001  rngohomco  38020  rngoisocnv  38027  rngoidl  38070  0idl  38071  intidl  38075  unichnidl  38077  keridl  38078  smprngopr  38098  lshpnel2N  39090  lkrshp  39210  4atexlemex2  40176  4atex  40181  cdleme0moN  40330  istendod  40867  dihlspsnat  41438  dochsatshp  41556  mon1psubm  43297  iocinico  43310  dfrtrcl3  43831  eliood  45603  eliccd  45609  eliocd  45612  limciccioolb  45726  limcicciooub  45740  icccncfext  45990  iblspltprt  46076  itgspltprt  46082  fourierdlem1  46211  fourierdlem4  46214  fourierdlem32  46242  fourierdlem33  46243  fourierdlem43  46253  fourierdlem65  46274  fourierdlem79  46288  prsal  46421  issald  46436  iccpartrn  47535  fpprwpprb  47845  bgoldbtbnd  47914  upgrimwlk  48007  upgrimpths  48014  gpgedgvtx0  48166  gpgedgvtx1  48167  gpgprismgr4cycllem11  48210  expnegico01  48624  dignnld  48709  reorelicc  48816