Theorem mpbir3and 1340

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  2ellim  8513  canthwelem  10665  intwun  10750  tskwun  10799  gruwun  10828  ixxss1  13366  ixxss2  13367  ixxss12  13368  ixxub  13369  ixxlb  13370  elicod  13398  ubioc1  13401  lbico1  13402  lbicc2  13465  ubicc2  13466  difreicc  13485  supicc  13502  modelico  13870  zmodfz  13882  addmodid  13908  dfrtrcl2  15033  phicl2  16728  4sqlem12  16916  isfuncd  17842  idfucl  17858  cofucl  17865  invfuc  17957  cnvps  18561  psss  18563  issubmd  18749  mndissubm  18750  submid  18753  subsubm  18759  0subm  18760  mhmima  18768  mhmeql  18769  gsumwspan  18789  frmdsssubm  18804  sursubmefmnd  18839  injsubmefmnd  18840  issubgrpd2  19088  grpissubg  19092  subgint  19096  0subgOLD  19098  nmzsubg  19111  eqger  19124  eqgcpbl  19128  cycsubm  19148  cycsubgcl  19152  ghmrn  19174  ghmpreima  19183  gastacl  19251  cntzsubm  19280  sylow2blem1  19566  lsmsubm  19599  torsubg  19800  oddvdssubg  19801  dmdprdd  19947  dprdsubg  19972  dprdres  19976  unitsubm  20314  cntzsubrng  20493  subrgsubm  20513  subrgugrp  20519  subrgint  20523  cntzsubr  20534  issubdrg  20657  lsssubg  20830  islmhm2  20912  pj1lmhm  20974  islbs2  21031  islbs3  21032  lbsextlem4  21038  issubrgd  21071  lidlsubg  21108  2idlcpblrng  21154  isphld  21573  mplsubglem  21928  mplsubrg  21934  mplind  22001  mhpsubg  22064  dmatsgrp  22388  dmatsrng  22390  scmatsgrp  22408  scmatsrng  22409  scmatsgrp1  22411  scmatsrng1  22412  cpmatsubgpmat  22609  cpmatsrgpmat  22610  lmcnp  23195  isufil2  23799  ufileu  23810  filufint  23811  fmfnfm  23849  flimclslem  23875  fclsfnflim  23918  flimfnfcls  23919  fclscmp  23921  clssubg  24000  tgpconncompeqg  24003  tgpconncomp  24004  qustgpopn  24011  tgptsmscls  24041  xmeter  24326  metust  24454  tgqioo  24703  zcld  24716  iccntr  24724  icccmplem2  24726  icccmplem3  24727  reconnlem1  24729  reconnlem2  24730  xrge0tsms  24737  cnheiborlem  24867  om1addcl  24947  pi1blem  24953  pi1grplem  24963  pi1inv  24966  pi1xfr  24969  pi1xfrcnvlem  24970  pi1coghm  24975  cmetcaulem  25203  ivthlem2  25368  ivthlem3  25369  ovolicc2lem2  25434  ovolicc2lem5  25437  opnmbllem  25517  volcn  25522  ismbf3d  25570  mbfi1fseqlem6  25637  itg2const2  25658  i1fibl  25724  ibladd  25737  bddiblnc  25758  ditgsplitlem  25776  dvferm1lem  25903  dvferm2lem  25905  dvlip2  25915  dvivthlem1  25928  dvne0  25931  lhop1lem  25933  lhop1  25934  lhop  25936  dvcnvrelem1  25937  dvcnvrelem2  25938  dvcnvre  25939  ftc1lem1  25957  itgsubst  25971  aaliou3lem2  26265  psercnlem2  26348  efif1olem2  26464  logtayl  26581  log2tlbnd  26864  xrlimcnp  26887  pntibndlem2  27511  pntlemj  27523  pntleml  27531  bday0b  27750  cuteq0  27752  cuteq1  27753  madebdaylemlrcut  27812  cofcut1  27827  trgcgr  28307  hlid  28400  hltr  28401  btwnhl1  28403  btwnhl2  28404  hlcgrex  28407  mirhl  28470  mirbtwnhl  28471  mirhl2  28472  hlpasch  28547  lnopp2hpgb  28554  cgrahl  28618  axlowdim  28759  uhgrissubgr  29075  egrsubgr  29077  uhgrspansubgr  29091  uhgrspan1  29103  cusgrrusgr  29382  wlkonwlk  29463  wlkonwlk1l  29464  wlkres  29471  wlkp1  29482  wlkd  29487  lfgriswlk  29489  wwlksnextinj  29697  2wlkond  29735  wpthswwlks2on  29759  0wlkon  29917  1wlkd  29938  1pthond  29941  eliccelico  32529  elicoelioo  32530  xrge0tsmsd  32749  tpr2rico  33449  measinb  33776  cntmeas  33781  dya2icoseg  33833  sibf0  33890  sibfof  33896  pfxwlk  34669  revwlk  34670  resconn  34792  cvmsss2  34820  cvmliftlem10  34840  mrsubco  35067  cgrextend  35540  cgr3rflx  35586  cgrxfr  35587  btwnconn1lem4  35622  btwnconn1lem8  35626  btwnconn1lem11  35629  bj-pinftynminfty  36642  bj-rveccmod  36717  iooelexlt  36777  opnmbllem0  37064  ibladdnc  37085  ftc1anc  37109  isbnd3  37192  prdsbnd  37201  rngomndo  37343  isgrpda  37363  rngohomco  37382  rngoisocnv  37389  rngoidl  37432  0idl  37433  intidl  37437  unichnidl  37439  keridl  37440  smprngopr  37460  lshpnel2N  38394  lkrshp  38514  4atexlemex2  39481  4atex  39486  cdleme0moN  39635  istendod  40172  dihlspsnat  40743  dochsatshp  40861  mon1psubm  42550  iocinico  42563  dfrtrcl3  43086  eliood  44806  eliccd  44812  eliocd  44815  limciccioolb  44932  limcicciooub  44948  icccncfext  45198  iblspltprt  45284  itgspltprt  45290  fourierdlem1  45419  fourierdlem4  45422  fourierdlem32  45450  fourierdlem33  45451  fourierdlem43  45461  fourierdlem65  45482  fourierdlem79  45496  prsal  45629  issald  45644  iccpartrn  46693  fpprwpprb  47003  bgoldbtbnd  47072  expnegico01  47509  dignnld  47599  reorelicc  47706