Theorem mpbir3and 1352

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1095

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 209  df-an 399  df-3an 1097

This theorem is referenced by:  2ellim  8452  canthwelem  10594  intwun  10679  tskwun  10728  gruwun  10757  ixxss1  13353  ixxss2  13354  ixxss12  13355  ixxub  13356  ixxlb  13357  elicod  13385  ubioc1  13389  lbico1  13390  lbicc2  13454  ubicc2  13455  difreicc  13474  supicc  13491  nnge2recico01  13497  modelico  13877  zmodfz  13889  addmodid  13918  dfrtrcl2  15061  phicl2  16775  4sqlem12  16964  isfuncd  17870  idfucl  17886  cofucl  17893  invfuc  17982  cnvps  18582  psss  18584  issubmd  18812  mndissubm  18813  submid  18816  subsubm  18822  0subm  18823  mhmima  18831  mhmeql  18832  gsumwspan  18852  frmdsssubm  18867  sursubmefmnd  18902  injsubmefmnd  18903  issubgrpd2  19156  grpissubg  19160  subgint  19164  nmzsubg  19178  eqger  19191  eqgcpbl  19195  cycsubm  19215  cycsubgcl  19219  ghmrn  19241  ghmpreima  19250  gastacl  19321  cntzsubm  19350  sylow2blem1  19632  lsmsubm  19665  torsubg  19866  oddvdssubg  19867  dmdprdd  20013  dprdsubg  20038  dprdres  20042  unitsubm  20403  cntzsubrng  20585  subrgsubm  20603  subrgugrp  20609  subrgint  20613  cntzsubr  20624  issubdrg  20798  lsssubg  20993  islmhm2  21074  pj1lmhm  21136  islbs2  21193  islbs3  21194  lbsextlem4  21200  issubrgd  21225  lidlsubg  21262  2idlcpblrng  21310  isphld  21675  mplsubglem  22019  mplsubrg  22025  mplind  22092  mhpsubg  22187  dmatsgrp  22528  dmatsrng  22530  scmatsgrp  22548  scmatsrng  22549  scmatsgrp1  22551  scmatsrng1  22552  cpmatsubgpmat  22749  cpmatsrgpmat  22750  lmcnp  23333  isufil2  23937  ufileu  23948  filufint  23949  fmfnfm  23987  flimclslem  24013  fclsfnflim  24056  flimfnfcls  24057  fclscmp  24059  clssubg  24138  tgpconncompeqg  24141  tgpconncomp  24142  qustgpopn  24149  tgptsmscls  24179  xmeter  24462  metust  24587  tgqioo  24829  zcld  24843  iccntr  24851  icccmplem2  24853  icccmplem3  24854  reconnlem1  24856  reconnlem2  24857  xrge0tsms  24864  cnheiborlem  24985  om1addcl  25064  pi1blem  25070  pi1grplem  25080  pi1inv  25083  pi1xfr  25086  pi1xfrcnvlem  25087  pi1coghm  25092  cmetcaulem  25319  ivthlem2  25483  ivthlem3  25484  ovolicc2lem2  25549  ovolicc2lem5  25552  opnmbllem  25632  volcn  25637  ismbf3d  25685  mbfi1fseqlem6  25751  itg2const2  25772  i1fibl  25839  ibladd  25852  bddiblnc  25873  ditgsplitlem  25891  dvferm1lem  26015  dvferm2lem  26017  dvlip2  26026  dvivthlem1  26039  dvne0  26042  lhop1lem  26044  lhop1  26045  lhop  26047  dvcnvrelem1  26048  dvcnvrelem2  26049  dvcnvre  26050  ftc1lem1  26066  itgsubst  26080  aaliou3lem2  26373  psercnlem2  26453  efif1olem2  26574  logtayl  26691  log2tlbnd  26976  xrlimcnp  26999  pntibndlem2  27621  pntlemj  27633  pntleml  27641  bday0b  27872  cuteq0  27874  cuteq1  27876  madebdaylemlrcut  27958  cofcut1  27979  oncutlt  28323  trgcgr  28651  hlid  28744  hltr  28745  btwnhl1  28747  btwnhl2  28748  hlcgrex  28751  mirhl  28814  mirbtwnhl  28815  mirhl2  28816  hlpasch  28891  lnopp2hpgb  28898  cgrahl  28962  axlowdim  29097  uhgrissubgr  29411  egrsubgr  29413  uhgrspansubgr  29427  uhgrspan1  29439  cusgrrusgr  29717  wlkonwlk  29796  wlkonwlk1l  29797  wlkres  29804  wlkp1  29815  wlkd  29820  lfgriswlk  29822  wwlksnextinj  30034  2wlkond  30072  wpthswwlks2on  30099  0wlkon  30257  1wlkd  30278  1pthond  30281  eliccelico  32918  elicoelioo  32919  xrge0tsmsd  33203  tpr2rico  34153  measinb  34462  cntmeas  34467  dya2icoseg  34518  sibf0  34575  sibfof  34581  pfxwlk  35412  revwlk  35413  resconn  35534  cvmsss2  35562  cvmliftlem10  35582  mrsubco  35809  cgrextend  36296  cgr3rflx  36342  cgrxfr  36343  btwnconn1lem4  36378  btwnconn1lem8  36382  btwnconn1lem11  36385  bj-pinftynminfty  37657  bj-rveccmod  37732  iooelexlt  37794  opnmbllem0  38093  ibladdnc  38114  ftc1anc  38138  isbnd3  38221  prdsbnd  38230  rngomndo  38372  isgrpda  38392  rngohomco  38411  rngoisocnv  38418  rngoidl  38461  0idl  38462  intidl  38466  unichnidl  38468  keridl  38469  smprngopr  38489  lshpnel2N  39547  lkrshp  39667  4atexlemex2  40633  4atex  40638  cdleme0moN  40787  istendod  41324  dihlspsnat  41895  dochsatshp  42013  mon1psubm  43714  iocinico  43727  dfrtrcl3  44247  eliood  46012  eliccd  46018  eliocd  46021  limciccioolb  46135  limcicciooub  46149  icccncfext  46399  iblspltprt  46485  itgspltprt  46491  fourierdlem1  46620  fourierdlem4  46623  fourierdlem32  46651  fourierdlem33  46652  fourierdlem43  46662  fourierdlem65  46683  fourierdlem79  46697  prsal  46830  issald  46845  flmrecm1  47875  iccpartrn  47974  fpprwpprb  48300  bgoldbtbnd  48369  upgrimwlk  48462  upgrimpths  48469  gpgedgvtx0  48621  gpgedgvtx1  48622  gpgprismgr4cycllem11  48665  expnegico01  49078  dignnld  49163  reorelicc  49270