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  8423  canthwelem  10562  intwun  10647  tskwun  10696  gruwun  10725  ixxss1  13305  ixxss2  13306  ixxss12  13307  ixxub  13308  ixxlb  13309  elicod  13337  ubioc1  13341  lbico1  13342  lbicc2  13406  ubicc2  13407  difreicc  13426  supicc  13443  nnge2recico01  13449  modelico  13829  zmodfz  13841  addmodid  13870  dfrtrcl2  15013  phicl2  16727  4sqlem12  16916  isfuncd  17821  idfucl  17837  cofucl  17844  invfuc  17933  cnvps  18533  psss  18535  issubmd  18763  mndissubm  18764  submid  18767  subsubm  18773  0subm  18774  mhmima  18782  mhmeql  18783  gsumwspan  18803  frmdsssubm  18818  sursubmefmnd  18853  injsubmefmnd  18854  issubgrpd2  19107  grpissubg  19111  subgint  19115  nmzsubg  19129  eqger  19142  eqgcpbl  19146  cycsubm  19166  cycsubgcl  19170  ghmrn  19193  ghmpreima  19202  gastacl  19273  cntzsubm  19302  sylow2blem1  19584  lsmsubm  19617  torsubg  19818  oddvdssubg  19819  dmdprdd  19965  dprdsubg  19990  dprdres  19994  unitsubm  20355  cntzsubrng  20533  subrgsubm  20551  subrgugrp  20557  subrgint  20561  cntzsubr  20572  issubdrg  20746  lsssubg  20941  islmhm2  21022  pj1lmhm  21084  islbs2  21141  islbs3  21142  lbsextlem4  21148  issubrgd  21173  lidlsubg  21210  2idlcpblrng  21258  isphld  21623  mplsubglem  21966  mplsubrg  21972  mplind  22037  mhpsubg  22108  dmatsgrp  22452  dmatsrng  22454  scmatsgrp  22472  scmatsrng  22473  scmatsgrp1  22475  scmatsrng1  22476  cpmatsubgpmat  22673  cpmatsrgpmat  22674  lmcnp  23257  isufil2  23861  ufileu  23872  filufint  23873  fmfnfm  23911  flimclslem  23937  fclsfnflim  23980  flimfnfcls  23981  fclscmp  23983  clssubg  24062  tgpconncompeqg  24065  tgpconncomp  24066  qustgpopn  24073  tgptsmscls  24103  xmeter  24386  metust  24511  tgqioo  24753  zcld  24767  iccntr  24775  icccmplem2  24777  icccmplem3  24778  reconnlem1  24780  reconnlem2  24781  xrge0tsms  24788  cnheiborlem  24909  om1addcl  24988  pi1blem  24994  pi1grplem  25004  pi1inv  25007  pi1xfr  25010  pi1xfrcnvlem  25011  pi1coghm  25016  cmetcaulem  25243  ivthlem2  25407  ivthlem3  25408  ovolicc2lem2  25473  ovolicc2lem5  25476  opnmbllem  25556  volcn  25561  ismbf3d  25609  mbfi1fseqlem6  25675  itg2const2  25696  i1fibl  25763  ibladd  25776  bddiblnc  25797  ditgsplitlem  25815  dvferm1lem  25939  dvferm2lem  25941  dvlip2  25950  dvivthlem1  25963  dvne0  25966  lhop1lem  25968  lhop1  25969  lhop  25971  dvcnvrelem1  25972  dvcnvrelem2  25973  dvcnvre  25974  ftc1lem1  25990  itgsubst  26004  aaliou3lem2  26297  psercnlem2  26377  efif1olem2  26495  logtayl  26612  log2tlbnd  26897  xrlimcnp  26920  pntibndlem2  27542  pntlemj  27554  pntleml  27562  bday0b  27793  cuteq0  27795  cuteq1  27797  madebdaylemlrcut  27879  cofcut1  27900  oncutlt  28244  trgcgr  28572  hlid  28665  hltr  28666  btwnhl1  28668  btwnhl2  28669  hlcgrex  28672  mirhl  28735  mirbtwnhl  28736  mirhl2  28737  hlpasch  28812  lnopp2hpgb  28819  cgrahl  28883  axlowdim  29018  uhgrissubgr  29332  egrsubgr  29334  uhgrspansubgr  29348  uhgrspan1  29360  cusgrrusgr  29638  wlkonwlk  29717  wlkonwlk1l  29718  wlkres  29725  wlkp1  29736  wlkd  29741  lfgriswlk  29743  wwlksnextinj  29955  2wlkond  29993  wpthswwlks2on  30020  0wlkon  30178  1wlkd  30199  1pthond  30202  eliccelico  32838  elicoelioo  32839  xrge0tsmsd  33122  tpr2rico  34044  measinb  34353  cntmeas  34358  dya2icoseg  34409  sibf0  34466  sibfof  34472  pfxwlk  35294  revwlk  35295  resconn  35416  cvmsss2  35444  cvmliftlem10  35464  mrsubco  35691  cgrextend  36178  cgr3rflx  36224  cgrxfr  36225  btwnconn1lem4  36260  btwnconn1lem8  36264  btwnconn1lem11  36267  bj-pinftynminfty  37529  bj-rveccmod  37604  iooelexlt  37666  opnmbllem0  37965  ibladdnc  37986  ftc1anc  38010  isbnd3  38093  prdsbnd  38102  rngomndo  38244  isgrpda  38264  rngohomco  38283  rngoisocnv  38290  rngoidl  38333  0idl  38334  intidl  38338  unichnidl  38340  keridl  38341  smprngopr  38361  lshpnel2N  39419  lkrshp  39539  4atexlemex2  40505  4atex  40510  cdleme0moN  40659  istendod  41196  dihlspsnat  41767  dochsatshp  41885  mon1psubm  43615  iocinico  43628  dfrtrcl3  44148  eliood  45916  eliccd  45922  eliocd  45925  limciccioolb  46039  limcicciooub  46053  icccncfext  46303  iblspltprt  46389  itgspltprt  46395  fourierdlem1  46524  fourierdlem4  46527  fourierdlem32  46555  fourierdlem33  46556  fourierdlem43  46566  fourierdlem65  46587  fourierdlem79  46601  prsal  46734  issald  46749  flmrecm1  47779  iccpartrn  47878  fpprwpprb  48204  bgoldbtbnd  48273  upgrimwlk  48366  upgrimpths  48373  gpgedgvtx0  48525  gpgedgvtx1  48526  gpgprismgr4cycllem11  48569  expnegico01  48982  dignnld  49067  reorelicc  49174