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  8509  canthwelem  10662  intwun  10747  tskwun  10796  gruwun  10825  ixxss1  13378  ixxss2  13379  ixxss12  13380  ixxub  13381  ixxlb  13382  elicod  13410  ubioc1  13414  lbico1  13415  lbicc2  13479  ubicc2  13480  difreicc  13499  supicc  13516  modelico  13896  zmodfz  13908  addmodid  13935  dfrtrcl2  15079  phicl2  16785  4sqlem12  16974  isfuncd  17876  idfucl  17892  cofucl  17899  invfuc  17988  cnvps  18586  psss  18588  issubmd  18782  mndissubm  18783  submid  18786  subsubm  18792  0subm  18793  mhmima  18801  mhmeql  18802  gsumwspan  18822  frmdsssubm  18837  sursubmefmnd  18872  injsubmefmnd  18873  issubgrpd2  19123  grpissubg  19127  subgint  19131  0subgOLD  19133  nmzsubg  19146  eqger  19159  eqgcpbl  19163  cycsubm  19183  cycsubgcl  19187  ghmrn  19210  ghmpreima  19219  gastacl  19290  cntzsubm  19319  sylow2blem1  19599  lsmsubm  19632  torsubg  19833  oddvdssubg  19834  dmdprdd  19980  dprdsubg  20005  dprdres  20009  unitsubm  20344  cntzsubrng  20525  subrgsubm  20543  subrgugrp  20549  subrgint  20553  cntzsubr  20564  issubdrg  20738  lsssubg  20912  islmhm2  20994  pj1lmhm  21056  islbs2  21113  islbs3  21114  lbsextlem4  21120  issubrgd  21145  lidlsubg  21182  2idlcpblrng  21230  isphld  21612  mplsubglem  21957  mplsubrg  21963  mplind  22026  mhpsubg  22089  dmatsgrp  22435  dmatsrng  22437  scmatsgrp  22455  scmatsrng  22456  scmatsgrp1  22458  scmatsrng1  22459  cpmatsubgpmat  22656  cpmatsrgpmat  22657  lmcnp  23240  isufil2  23844  ufileu  23855  filufint  23856  fmfnfm  23894  flimclslem  23920  fclsfnflim  23963  flimfnfcls  23964  fclscmp  23966  clssubg  24045  tgpconncompeqg  24048  tgpconncomp  24049  qustgpopn  24056  tgptsmscls  24086  xmeter  24370  metust  24495  tgqioo  24737  zcld  24751  iccntr  24759  icccmplem2  24761  icccmplem3  24762  reconnlem1  24764  reconnlem2  24765  xrge0tsms  24772  cnheiborlem  24902  om1addcl  24982  pi1blem  24988  pi1grplem  24998  pi1inv  25001  pi1xfr  25004  pi1xfrcnvlem  25005  pi1coghm  25010  cmetcaulem  25238  ivthlem2  25403  ivthlem3  25404  ovolicc2lem2  25469  ovolicc2lem5  25472  opnmbllem  25552  volcn  25557  ismbf3d  25605  mbfi1fseqlem6  25671  itg2const2  25692  i1fibl  25759  ibladd  25772  bddiblnc  25793  ditgsplitlem  25811  dvferm1lem  25938  dvferm2lem  25940  dvlip2  25950  dvivthlem1  25963  dvne0  25966  lhop1lem  25968  lhop1  25969  lhop  25971  dvcnvrelem1  25972  dvcnvrelem2  25973  dvcnvre  25974  ftc1lem1  25992  itgsubst  26006  aaliou3lem2  26301  psercnlem2  26384  efif1olem2  26502  logtayl  26619  log2tlbnd  26905  xrlimcnp  26928  pntibndlem2  27552  pntlemj  27564  pntleml  27572  bday0b  27792  cuteq0  27794  cuteq1  27795  madebdaylemlrcut  27854  cofcut1  27871  trgcgr  28441  hlid  28534  hltr  28535  btwnhl1  28537  btwnhl2  28538  hlcgrex  28541  mirhl  28604  mirbtwnhl  28605  mirhl2  28606  hlpasch  28681  lnopp2hpgb  28688  cgrahl  28752  axlowdim  28886  uhgrissubgr  29200  egrsubgr  29202  uhgrspansubgr  29216  uhgrspan1  29228  cusgrrusgr  29507  wlkonwlk  29588  wlkonwlk1l  29589  wlkres  29596  wlkp1  29607  wlkd  29612  lfgriswlk  29614  wwlksnextinj  29827  2wlkond  29865  wpthswwlks2on  29889  0wlkon  30047  1wlkd  30068  1pthond  30071  eliccelico  32700  elicoelioo  32701  xrge0tsmsd  33002  tpr2rico  33889  measinb  34198  cntmeas  34203  dya2icoseg  34255  sibf0  34312  sibfof  34318  pfxwlk  35092  revwlk  35093  resconn  35214  cvmsss2  35242  cvmliftlem10  35262  mrsubco  35489  cgrextend  35972  cgr3rflx  36018  cgrxfr  36019  btwnconn1lem4  36054  btwnconn1lem8  36058  btwnconn1lem11  36061  bj-pinftynminfty  37191  bj-rveccmod  37266  iooelexlt  37326  opnmbllem0  37626  ibladdnc  37647  ftc1anc  37671  isbnd3  37754  prdsbnd  37763  rngomndo  37905  isgrpda  37925  rngohomco  37944  rngoisocnv  37951  rngoidl  37994  0idl  37995  intidl  37999  unichnidl  38001  keridl  38002  smprngopr  38022  lshpnel2N  38949  lkrshp  39069  4atexlemex2  40036  4atex  40041  cdleme0moN  40190  istendod  40727  dihlspsnat  41298  dochsatshp  41416  mon1psubm  43170  iocinico  43183  dfrtrcl3  43704  eliood  45475  eliccd  45481  eliocd  45484  limciccioolb  45598  limcicciooub  45614  icccncfext  45864  iblspltprt  45950  itgspltprt  45956  fourierdlem1  46085  fourierdlem4  46088  fourierdlem32  46116  fourierdlem33  46117  fourierdlem43  46127  fourierdlem65  46148  fourierdlem79  46162  prsal  46295  issald  46310  iccpartrn  47392  fpprwpprb  47702  bgoldbtbnd  47771  upgrimwlk  47863  upgrimpths  47870  gpgedgvtx0  48013  gpgedgvtx1  48014  gpgprismgr4cycllem11  48052  expnegico01  48442  dignnld  48531  reorelicc  48638