Theorem mpbir3and 1339

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  canthwelem  10061  intwun  10146  tskwun  10195  gruwun  10224  ixxss1  12744  ixxss2  12745  ixxss12  12746  ixxub  12747  ixxlb  12748  elicod  12775  ubioc1  12778  lbico1  12779  lbicc2  12842  ubicc2  12843  difreicc  12862  supicc  12879  modelico  13244  zmodfz  13256  addmodid  13282  dfrtrcl2  14413  phicl2  16095  4sqlem12  16282  isfuncd  17127  idfucl  17143  cofucl  17150  invfuc  17236  cnvps  17814  psss  17816  issubmd  17963  mndissubm  17964  submid  17967  subsubm  17973  0subm  17974  mhmima  17981  mhmeql  17982  gsumwspan  18003  frmdsssubm  18018  sursubmefmnd  18053  injsubmefmnd  18054  issubgrpd2  18287  grpissubg  18291  subgint  18295  0subg  18296  nmzsubg  18309  eqger  18322  eqgcpbl  18326  cycsubm  18337  cycsubgcl  18341  ghmrn  18363  ghmpreima  18372  gastacl  18431  cntzsubm  18458  sylow2blem1  18737  lsmsubm  18770  torsubg  18967  oddvdssubg  18968  dmdprdd  19114  dprdsubg  19139  dprdres  19143  unitsubm  19416  subrgsubm  19541  subrgugrp  19547  subrgint  19550  issubdrg  19553  cntzsubr  19561  lsssubg  19722  islmhm2  19803  pj1lmhm  19865  islbs2  19919  islbs3  19920  lbsextlem4  19926  issubrngd2  19954  lidlsubg  19981  2idlcpbl  20000  isphld  20343  mplsubglem  20672  mplsubrg  20678  mplind  20741  mhpsubg  20801  dmatsgrp  21104  dmatsrng  21106  scmatsgrp  21124  scmatsrng  21125  scmatsgrp1  21127  scmatsrng1  21128  cpmatsubgpmat  21325  cpmatsrgpmat  21326  lmcnp  21909  isufil2  22513  ufileu  22524  filufint  22525  fmfnfm  22563  flimclslem  22589  fclsfnflim  22632  flimfnfcls  22633  fclscmp  22635  clssubg  22714  tgpconncompeqg  22717  tgpconncomp  22718  qustgpopn  22725  tgptsmscls  22755  xmeter  23040  metust  23165  tgqioo  23405  zcld  23418  iccntr  23426  icccmplem2  23428  icccmplem3  23429  reconnlem1  23431  reconnlem2  23432  xrge0tsms  23439  cnheiborlem  23559  om1addcl  23638  pi1blem  23644  pi1grplem  23654  pi1inv  23657  pi1xfr  23660  pi1xfrcnvlem  23661  pi1coghm  23666  cmetcaulem  23892  ivthlem2  24056  ivthlem3  24057  ovolicc2lem2  24122  ovolicc2lem5  24125  opnmbllem  24205  volcn  24210  ismbf3d  24258  mbfi1fseqlem6  24324  itg2const2  24345  i1fibl  24411  ibladd  24424  bddiblnc  24445  ditgsplitlem  24463  dvferm1lem  24587  dvferm2lem  24589  dvlip2  24598  dvivthlem1  24611  dvne0  24614  lhop1lem  24616  lhop1  24617  lhop  24619  dvcnvrelem1  24620  dvcnvrelem2  24621  dvcnvre  24622  ftc1lem1  24638  itgsubst  24652  aaliou3lem2  24939  psercnlem2  25019  efif1olem2  25135  logtayl  25251  log2tlbnd  25531  xrlimcnp  25554  pntibndlem2  26175  pntlemj  26187  pntleml  26195  trgcgr  26310  hlid  26403  hltr  26404  btwnhl1  26406  btwnhl2  26407  hlcgrex  26410  mirhl  26473  mirbtwnhl  26474  mirhl2  26475  hlpasch  26550  lnopp2hpgb  26557  cgrahl  26621  axlowdim  26755  uhgrissubgr  27065  egrsubgr  27067  uhgrspansubgr  27081  uhgrspan1  27093  cusgrrusgr  27371  wlkonwlk  27452  wlkonwlk1l  27453  wlkres  27460  wlkp1  27471  wlkd  27476  lfgriswlk  27478  wwlksnextinj  27685  2wlkond  27723  wpthswwlks2on  27747  0wlkon  27905  1wlkd  27926  1pthond  27929  eliccelico  30526  elicoelioo  30527  xrge0tsmsd  30742  tpr2rico  31265  measinb  31590  cntmeas  31595  dya2icoseg  31645  sibf0  31702  sibfof  31708  pfxwlk  32483  revwlk  32484  resconn  32606  cvmsss2  32634  cvmliftlem10  32654  mrsubco  32881  cgrextend  33582  cgr3rflx  33628  cgrxfr  33629  btwnconn1lem4  33664  btwnconn1lem8  33668  btwnconn1lem11  33671  bj-pinftynminfty  34642  bj-rveccmod  34716  iooelexlt  34779  opnmbllem0  35093  ibladdnc  35114  ftc1anc  35138  isbnd3  35222  prdsbnd  35231  rngomndo  35373  isgrpda  35393  rngohomco  35412  rngoisocnv  35419  rngoidl  35462  0idl  35463  intidl  35467  unichnidl  35469  keridl  35470  smprngopr  35490  lshpnel2N  36281  lkrshp  36401  4atexlemex2  37367  4atex  37372  cdleme0moN  37521  istendod  38058  dihlspsnat  38629  dochsatshp  38747  mon1psubm  40150  iocinico  40162  dfrtrcl3  40434  eliood  42135  eliccd  42141  eliocd  42144  limciccioolb  42263  limcicciooub  42279  icccncfext  42529  iblspltprt  42615  itgspltprt  42621  fourierdlem1  42750  fourierdlem4  42753  fourierdlem32  42781  fourierdlem33  42782  fourierdlem43  42792  fourierdlem65  42813  fourierdlem79  42827  prsal  42960  issald  42973  iccpartrn  43947  fpprwpprb  44258  bgoldbtbnd  44327  expnegico01  44927  dignnld  45017  reorelicc  45124