Theorem mpbir3and 1238

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  canthwelem  9351  intwun  9436  tskwun  9485  gruwun  9514  ixxss1  12064  ixxss2  12065  ixxss12  12066  ixxub  12067  ixxlb  12068  elicod  12095  ubioc1  12098  lbico1  12099  lbicc2  12159  ubicc2  12160  difreicc  12175  supicc  12191  modelico  12542  zmodfz  12554  addmodid  12580  dfrtrcl2  13650  phicl2  15311  4sqlem12  15498  isfuncd  16348  idfucl  16364  cofucl  16371  invfuc  16457  cnvps  17035  psss  17037  issubmd  17172  submid  17174  subsubm  17180  mhmima  17186  mhmeql  17187  gsumwspan  17206  frmdsssubm  17221  issubgrpd2  17433  grpissubg  17437  subgint  17441  0subg  17442  cycsubgcl  17443  nmzsubg  17458  eqger  17467  eqgcpbl  17471  ghmrn  17496  ghmpreima  17505  gastacl  17565  cntzsubm  17591  sylow2blem1  17858  lsmsubm  17891  torsubg  18080  oddvdssubg  18081  dmdprdd  18221  dprdsubg  18246  dprdres  18250  unitsubm  18493  subrgsubm  18616  subrgugrp  18622  subrgint  18625  issubdrg  18628  cntzsubr  18635  lsssubg  18778  islmhm2  18859  pj1lmhm  18921  islbs2  18975  islbs3  18976  lbsextlem4  18982  issubrngd2  19010  lidlsubg  19036  2idlcpbl  19055  mplsubglem  19255  mplsubrg  19261  mplind  19323  isphld  19818  dmatsgrp  20124  dmatsrng  20126  scmatsgrp  20144  scmatsrng  20145  scmatsgrp1  20147  scmatsrng1  20148  cpmatsubgpmat  20344  cpmatsrgpmat  20345  lmcnp  20918  isufil2  21522  ufileu  21533  filufint  21534  fmfnfm  21572  flimclslem  21598  fclsfnflim  21641  flimfnfcls  21642  fclscmp  21644  clssubg  21722  tgpconcompeqg  21725  tgpconcomp  21726  qustgpopn  21733  tgptsmscls  21763  xmeter  22048  metust  22173  tgqioo  22411  zcld  22424  iccntr  22432  icccmplem2  22434  icccmplem3  22435  reconnlem1  22437  reconnlem2  22438  xrge0tsms  22445  cnheiborlem  22561  om1addcl  22641  pi1blem  22647  pi1grplem  22657  pi1inv  22660  pi1xfr  22663  pi1xfrcnvlem  22664  pi1coghm  22669  cmetcaulem  22894  ivthlem2  23028  ivthlem3  23029  ovolicc2lem2  23093  ovolicc2lem5  23096  opnmbllem  23175  volcn  23180  ismbf3d  23227  mbfi1fseqlem6  23293  itg2const2  23314  i1fibl  23380  ibladd  23393  ditgsplitlem  23430  dvferm1lem  23551  dvferm2lem  23553  dvlip2  23562  dvivthlem1  23575  dvne0  23578  lhop1lem  23580  lhop1  23581  lhop  23583  dvcnvrelem1  23584  dvcnvrelem2  23585  dvcnvre  23586  ftc1lem1  23602  itgsubst  23616  aaliou3lem2  23902  psercnlem2  23982  efif1olem2  24093  logtayl  24206  log2tlbnd  24472  xrlimcnp  24495  pntibndlem2  25080  pntlemj  25092  pntleml  25100  trgcgr  25211  axlowdim  25641  wlkonwlk  26065  0wlkon  26077  constr1trl  26118  constr2wlk  26128  constr2trl  26129  constr2pth  26131  2pthon  26132  wwlkextinj  26258  el2spthonot  26397  cusgraisrusgra  26465  extwwlkfablem1  26601  eliccelico  28929  elicoelioo  28930  xrge0tsmsd  29116  tpr2rico  29286  measinb  29611  cntmeas  29616  dya2icoseg  29666  sibf0  29723  sibfof  29729  rescon  30482  cvmsss2  30510  cvmliftlem10  30530  mrsubco  30672  cgrextend  31285  cgr3rflx  31331  cgrxfr  31332  btwnconn1lem4  31367  btwnconn1lem8  31371  btwnconn1lem11  31374  bj-pinftynminfty  32291  iooelexlt  32386  opnmbllem0  32615  ibladdnc  32637  bddiblnc  32650  ftc1anc  32663  isbnd3  32753  prdsbnd  32762  rngomndo  32904  isgrpda  32924  rngohomco  32943  rngoisocnv  32950  rngoidl  32993  0idl  32994  intidl  32998  unichnidl  33000  keridl  33001  smprngopr  33021  lshpnel2N  33290  lkrshp  33410  4atexlemex2  34375  4atex  34380  cdleme0moN  34530  istendod  35068  dihlspsnat  35640  dochsatshp  35758  mon1psubm  36803  iocinico  36816  dfrtrcl3  37044  eliood  38567  eliccd  38573  eliocd  38577  limciccioolb  38688  limcicciooub  38704  icccncfext  38773  iblspltprt  38865  itgspltprt  38871  fourierdlem1  39001  fourierdlem4  39004  fourierdlem32  39032  fourierdlem33  39033  fourierdlem43  39043  fourierdlem65  39064  fourierdlem79  39078  iccpartrn  39968  bgoldbtbnd  40225  uhgrissubgr  40499  egrsubgr  40501  uhgrspansubgr  40515  uhgrspan1  40527  nbgr2vtx1edg  40572  nbuhgr2vtx1edgb  40574  cusgrexi  40662  cusgrrusgr  40781  wlkOnwlk  40870  wlkOnwlk1l  40871  1wlkres  40879  1wlkp1  40890  1wlkd  40895  lfgriswlk  40897  pthd  40975  wwlksnextinj  41105  21wlkond  41144  wpthswwlks2on  41164  0wlkOn  41288  11wlkd  41308  1pthd  41310  1pthond  41311  expnegico01  42102  dignnld  42195