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 256	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:  canthwelem  10390  intwun  10475  tskwun  10524  gruwun  10553  ixxss1  13079  ixxss2  13080  ixxss12  13081  ixxub  13082  ixxlb  13083  elicod  13111  ubioc1  13114  lbico1  13115  lbicc2  13178  ubicc2  13179  difreicc  13198  supicc  13215  modelico  13582  zmodfz  13594  addmodid  13620  dfrtrcl2  14754  phicl2  16450  4sqlem12  16638  isfuncd  17561  idfucl  17577  cofucl  17584  invfuc  17673  cnvps  18277  psss  18279  issubmd  18426  mndissubm  18427  submid  18430  subsubm  18436  0subm  18437  mhmima  18444  mhmeql  18445  gsumwspan  18466  frmdsssubm  18481  sursubmefmnd  18516  injsubmefmnd  18517  issubgrpd2  18752  grpissubg  18756  subgint  18760  0subg  18761  nmzsubg  18774  eqger  18787  eqgcpbl  18791  cycsubm  18802  cycsubgcl  18806  ghmrn  18828  ghmpreima  18837  gastacl  18896  cntzsubm  18923  sylow2blem1  19206  lsmsubm  19239  torsubg  19436  oddvdssubg  19437  dmdprdd  19583  dprdsubg  19608  dprdres  19612  unitsubm  19893  subrgsubm  20018  subrgugrp  20024  subrgint  20027  issubdrg  20030  cntzsubr  20038  lsssubg  20200  islmhm2  20281  pj1lmhm  20343  islbs2  20397  islbs3  20398  lbsextlem4  20404  issubrngd2  20440  lidlsubg  20467  2idlcpbl  20486  isphld  20840  mplsubglem  21186  mplsubrg  21192  mplind  21259  mhpsubg  21324  dmatsgrp  21629  dmatsrng  21631  scmatsgrp  21649  scmatsrng  21650  scmatsgrp1  21652  scmatsrng1  21653  cpmatsubgpmat  21850  cpmatsrgpmat  21851  lmcnp  22436  isufil2  23040  ufileu  23051  filufint  23052  fmfnfm  23090  flimclslem  23116  fclsfnflim  23159  flimfnfcls  23160  fclscmp  23162  clssubg  23241  tgpconncompeqg  23244  tgpconncomp  23245  qustgpopn  23252  tgptsmscls  23282  xmeter  23567  metust  23695  tgqioo  23944  zcld  23957  iccntr  23965  icccmplem2  23967  icccmplem3  23968  reconnlem1  23970  reconnlem2  23971  xrge0tsms  23978  cnheiborlem  24098  om1addcl  24177  pi1blem  24183  pi1grplem  24193  pi1inv  24196  pi1xfr  24199  pi1xfrcnvlem  24200  pi1coghm  24205  cmetcaulem  24433  ivthlem2  24597  ivthlem3  24598  ovolicc2lem2  24663  ovolicc2lem5  24666  opnmbllem  24746  volcn  24751  ismbf3d  24799  mbfi1fseqlem6  24866  itg2const2  24887  i1fibl  24953  ibladd  24966  bddiblnc  24987  ditgsplitlem  25005  dvferm1lem  25129  dvferm2lem  25131  dvlip2  25140  dvivthlem1  25153  dvne0  25156  lhop1lem  25158  lhop1  25159  lhop  25161  dvcnvrelem1  25162  dvcnvrelem2  25163  dvcnvre  25164  ftc1lem1  25180  itgsubst  25194  aaliou3lem2  25484  psercnlem2  25564  efif1olem2  25680  logtayl  25796  log2tlbnd  26076  xrlimcnp  26099  pntibndlem2  26720  pntlemj  26732  pntleml  26740  trgcgr  26858  hlid  26951  hltr  26952  btwnhl1  26954  btwnhl2  26955  hlcgrex  26958  mirhl  27021  mirbtwnhl  27022  mirhl2  27023  hlpasch  27098  lnopp2hpgb  27105  cgrahl  27169  axlowdim  27310  uhgrissubgr  27623  egrsubgr  27625  uhgrspansubgr  27639  uhgrspan1  27651  cusgrrusgr  27929  wlkonwlk  28010  wlkonwlk1l  28011  wlkres  28018  wlkp1  28029  wlkd  28034  lfgriswlk  28036  wwlksnextinj  28243  2wlkond  28281  wpthswwlks2on  28305  0wlkon  28463  1wlkd  28484  1pthond  28487  eliccelico  31077  elicoelioo  31078  xrge0tsmsd  31296  tpr2rico  31841  measinb  32168  cntmeas  32173  dya2icoseg  32223  sibf0  32280  sibfof  32286  pfxwlk  33064  revwlk  33065  resconn  33187  cvmsss2  33215  cvmliftlem10  33235  mrsubco  33462  bday0b  34003  madebdaylemlrcut  34058  cofcut1  34069  cgrextend  34289  cgr3rflx  34335  cgrxfr  34336  btwnconn1lem4  34371  btwnconn1lem8  34375  btwnconn1lem11  34378  bj-pinftynminfty  35377  bj-rveccmod  35452  iooelexlt  35512  opnmbllem0  35792  ibladdnc  35813  ftc1anc  35837  isbnd3  35921  prdsbnd  35930  rngomndo  36072  isgrpda  36092  rngohomco  36111  rngoisocnv  36118  rngoidl  36161  0idl  36162  intidl  36166  unichnidl  36168  keridl  36169  smprngopr  36189  lshpnel2N  36978  lkrshp  37098  4atexlemex2  38064  4atex  38069  cdleme0moN  38218  istendod  38755  dihlspsnat  39326  dochsatshp  39444  mon1psubm  41011  iocinico  41023  dfrtrcl3  41294  eliood  42990  eliccd  42996  eliocd  42999  limciccioolb  43116  limcicciooub  43132  icccncfext  43382  iblspltprt  43468  itgspltprt  43474  fourierdlem1  43603  fourierdlem4  43606  fourierdlem32  43634  fourierdlem33  43635  fourierdlem43  43645  fourierdlem65  43666  fourierdlem79  43680  prsal  43813  issald  43826  iccpartrn  44834  fpprwpprb  45144  bgoldbtbnd  45213  expnegico01  45811  dignnld  45901  reorelicc  46008