Theorem mpbir3and 1343

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  2ellim  8537  canthwelem  10690  intwun  10775  tskwun  10824  gruwun  10853  ixxss1  13405  ixxss2  13406  ixxss12  13407  ixxub  13408  ixxlb  13409  elicod  13437  ubioc1  13440  lbico1  13441  lbicc2  13504  ubicc2  13505  difreicc  13524  supicc  13541  modelico  13921  zmodfz  13933  addmodid  13960  dfrtrcl2  15101  phicl2  16805  4sqlem12  16994  isfuncd  17910  idfucl  17926  cofucl  17933  invfuc  18022  cnvps  18623  psss  18625  issubmd  18819  mndissubm  18820  submid  18823  subsubm  18829  0subm  18830  mhmima  18838  mhmeql  18839  gsumwspan  18859  frmdsssubm  18874  sursubmefmnd  18909  injsubmefmnd  18910  issubgrpd2  19160  grpissubg  19164  subgint  19168  0subgOLD  19170  nmzsubg  19183  eqger  19196  eqgcpbl  19200  cycsubm  19220  cycsubgcl  19224  ghmrn  19247  ghmpreima  19256  gastacl  19327  cntzsubm  19356  sylow2blem1  19638  lsmsubm  19671  torsubg  19872  oddvdssubg  19873  dmdprdd  20019  dprdsubg  20044  dprdres  20048  unitsubm  20386  cntzsubrng  20567  subrgsubm  20585  subrgugrp  20591  subrgint  20595  cntzsubr  20606  issubdrg  20781  lsssubg  20955  islmhm2  21037  pj1lmhm  21099  islbs2  21156  islbs3  21157  lbsextlem4  21163  issubrgd  21196  lidlsubg  21233  2idlcpblrng  21281  isphld  21672  mplsubglem  22019  mplsubrg  22025  mplind  22094  mhpsubg  22157  dmatsgrp  22505  dmatsrng  22507  scmatsgrp  22525  scmatsrng  22526  scmatsgrp1  22528  scmatsrng1  22529  cpmatsubgpmat  22726  cpmatsrgpmat  22727  lmcnp  23312  isufil2  23916  ufileu  23927  filufint  23928  fmfnfm  23966  flimclslem  23992  fclsfnflim  24035  flimfnfcls  24036  fclscmp  24038  clssubg  24117  tgpconncompeqg  24120  tgpconncomp  24121  qustgpopn  24128  tgptsmscls  24158  xmeter  24443  metust  24571  tgqioo  24821  zcld  24835  iccntr  24843  icccmplem2  24845  icccmplem3  24846  reconnlem1  24848  reconnlem2  24849  xrge0tsms  24856  cnheiborlem  24986  om1addcl  25066  pi1blem  25072  pi1grplem  25082  pi1inv  25085  pi1xfr  25088  pi1xfrcnvlem  25089  pi1coghm  25094  cmetcaulem  25322  ivthlem2  25487  ivthlem3  25488  ovolicc2lem2  25553  ovolicc2lem5  25556  opnmbllem  25636  volcn  25641  ismbf3d  25689  mbfi1fseqlem6  25755  itg2const2  25776  i1fibl  25843  ibladd  25856  bddiblnc  25877  ditgsplitlem  25895  dvferm1lem  26022  dvferm2lem  26024  dvlip2  26034  dvivthlem1  26047  dvne0  26050  lhop1lem  26052  lhop1  26053  lhop  26055  dvcnvrelem1  26056  dvcnvrelem2  26057  dvcnvre  26058  ftc1lem1  26076  itgsubst  26090  aaliou3lem2  26385  psercnlem2  26468  efif1olem2  26585  logtayl  26702  log2tlbnd  26988  xrlimcnp  27011  pntibndlem2  27635  pntlemj  27647  pntleml  27655  bday0b  27875  cuteq0  27877  cuteq1  27878  madebdaylemlrcut  27937  cofcut1  27954  trgcgr  28524  hlid  28617  hltr  28618  btwnhl1  28620  btwnhl2  28621  hlcgrex  28624  mirhl  28687  mirbtwnhl  28688  mirhl2  28689  hlpasch  28764  lnopp2hpgb  28771  cgrahl  28835  axlowdim  28976  uhgrissubgr  29292  egrsubgr  29294  uhgrspansubgr  29308  uhgrspan1  29320  cusgrrusgr  29599  wlkonwlk  29680  wlkonwlk1l  29681  wlkres  29688  wlkp1  29699  wlkd  29704  lfgriswlk  29706  wwlksnextinj  29919  2wlkond  29957  wpthswwlks2on  29981  0wlkon  30139  1wlkd  30160  1pthond  30163  eliccelico  32779  elicoelioo  32780  xrge0tsmsd  33065  tpr2rico  33911  measinb  34222  cntmeas  34227  dya2icoseg  34279  sibf0  34336  sibfof  34342  pfxwlk  35129  revwlk  35130  resconn  35251  cvmsss2  35279  cvmliftlem10  35299  mrsubco  35526  cgrextend  36009  cgr3rflx  36055  cgrxfr  36056  btwnconn1lem4  36091  btwnconn1lem8  36095  btwnconn1lem11  36098  bj-pinftynminfty  37228  bj-rveccmod  37303  iooelexlt  37363  opnmbllem0  37663  ibladdnc  37684  ftc1anc  37708  isbnd3  37791  prdsbnd  37800  rngomndo  37942  isgrpda  37962  rngohomco  37981  rngoisocnv  37988  rngoidl  38031  0idl  38032  intidl  38036  unichnidl  38038  keridl  38039  smprngopr  38059  lshpnel2N  38986  lkrshp  39106  4atexlemex2  40073  4atex  40078  cdleme0moN  40227  istendod  40764  dihlspsnat  41335  dochsatshp  41453  mon1psubm  43211  iocinico  43224  dfrtrcl3  43746  eliood  45511  eliccd  45517  eliocd  45520  limciccioolb  45636  limcicciooub  45652  icccncfext  45902  iblspltprt  45988  itgspltprt  45994  fourierdlem1  46123  fourierdlem4  46126  fourierdlem32  46154  fourierdlem33  46155  fourierdlem43  46165  fourierdlem65  46186  fourierdlem79  46200  prsal  46333  issald  46348  iccpartrn  47417  fpprwpprb  47727  bgoldbtbnd  47796  gpgedgvtx0  48019  gpgedgvtx1  48020  expnegico01  48435  dignnld  48524  reorelicc  48631