Theorem mpbir3and 1399

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  canthwelem  9807  intwun  9892  tskwun  9941  gruwun  9970  ixxss1  12505  ixxss2  12506  ixxss12  12507  ixxub  12508  ixxlb  12509  elicod  12536  ubioc1  12539  lbico1  12540  lbicc2  12602  ubicc2  12603  difreicc  12621  supicc  12637  modelico  12999  zmodfz  13011  addmodid  13037  dfrtrcl2  14209  phicl2  15877  4sqlem12  16064  isfuncd  16910  idfucl  16926  cofucl  16933  invfuc  17019  cnvps  17598  psss  17600  issubmd  17735  submid  17737  subsubm  17743  mhmima  17749  mhmeql  17750  gsumwspan  17770  frmdsssubm  17785  issubgrpd2  17994  grpissubg  17998  subgint  18002  0subg  18003  cycsubgcl  18004  nmzsubg  18019  eqger  18028  eqgcpbl  18032  ghmrn  18057  ghmpreima  18066  gastacl  18125  cntzsubm  18151  sylow2blem1  18419  lsmsubm  18452  torsubg  18643  oddvdssubg  18644  dmdprdd  18785  dprdsubg  18810  dprdres  18814  unitsubm  19057  subrgsubm  19185  subrgugrp  19191  subrgint  19194  issubdrg  19197  cntzsubr  19204  lsssubg  19352  islmhm2  19433  pj1lmhm  19495  islbs2  19551  islbs3  19552  lbsextlem4  19558  issubrngd2  19586  lidlsubg  19612  2idlcpbl  19631  mplsubglem  19831  mplsubrg  19837  mplind  19898  isphld  20397  dmatsgrp  20710  dmatsrng  20712  scmatsgrp  20730  scmatsrng  20731  scmatsgrp1  20733  scmatsrng1  20734  cpmatsubgpmat  20932  cpmatsrgpmat  20933  lmcnp  21516  isufil2  22120  ufileu  22131  filufint  22132  fmfnfm  22170  flimclslem  22196  fclsfnflim  22239  flimfnfcls  22240  fclscmp  22242  clssubg  22320  tgpconncompeqg  22323  tgpconncomp  22324  qustgpopn  22331  tgptsmscls  22361  xmeter  22646  metust  22771  tgqioo  23011  zcld  23024  iccntr  23032  icccmplem2  23034  icccmplem3  23035  reconnlem1  23037  reconnlem2  23038  xrge0tsms  23045  cnheiborlem  23161  om1addcl  23240  pi1blem  23246  pi1grplem  23256  pi1inv  23259  pi1xfr  23262  pi1xfrcnvlem  23263  pi1coghm  23268  cmetcaulem  23494  ivthlem2  23656  ivthlem3  23657  ovolicc2lem2  23722  ovolicc2lem5  23725  opnmbllem  23805  volcn  23810  ismbf3d  23858  mbfi1fseqlem6  23924  itg2const2  23945  i1fibl  24011  ibladd  24024  ditgsplitlem  24061  dvferm1lem  24184  dvferm2lem  24186  dvlip2  24195  dvivthlem1  24208  dvne0  24211  lhop1lem  24213  lhop1  24214  lhop  24216  dvcnvrelem1  24217  dvcnvrelem2  24218  dvcnvre  24219  ftc1lem1  24235  itgsubst  24249  aaliou3lem2  24535  psercnlem2  24615  efif1olem2  24727  logtayl  24843  log2tlbnd  25124  xrlimcnp  25147  pntibndlem2  25732  pntlemj  25744  pntleml  25752  trgcgr  25867  axlowdim  26310  uhgrissubgr  26622  egrsubgr  26624  uhgrspansubgr  26638  uhgrspan1  26650  cusgrrusgr  26929  wlkonwlk  27009  wlkonwlk1l  27010  wlkres  27019  wlkresOLD  27021  wlkp1  27032  wlkd  27037  lfgriswlk  27039  wwlksnextinj  27263  wwlksnextinjOLD  27268  2wlkond  27317  wpthswwlks2on  27341  0wlkon  27523  1wlkd  27544  1pthond  27547  eliccelico  30103  elicoelioo  30104  xrge0tsmsd  30347  tpr2rico  30556  measinb  30882  cntmeas  30887  dya2icoseg  30937  sibf0  30994  sibfof  31000  resconn  31827  cvmsss2  31855  cvmliftlem10  31875  mrsubco  32017  cgrextend  32704  cgr3rflx  32750  cgrxfr  32751  btwnconn1lem4  32786  btwnconn1lem8  32790  btwnconn1lem11  32793  bj-pinftynminfty  33704  iooelexlt  33805  opnmbllem0  34055  ibladdnc  34076  bddiblnc  34089  ftc1anc  34102  isbnd3  34191  prdsbnd  34200  rngomndo  34342  isgrpda  34362  rngohomco  34381  rngoisocnv  34388  rngoidl  34431  0idl  34432  intidl  34436  unichnidl  34438  keridl  34439  smprngopr  34459  lshpnel2N  35123  lkrshp  35243  4atexlemex2  36209  4atex  36214  cdleme0moN  36363  istendod  36900  dihlspsnat  37471  dochsatshp  37589  mon1psubm  38725  iocinico  38737  dfrtrcl3  38964  eliood  40614  eliccd  40620  eliocd  40624  limciccioolb  40743  limcicciooub  40759  icccncfext  41010  iblspltprt  41098  itgspltprt  41104  fourierdlem1  41234  fourierdlem4  41237  fourierdlem32  41265  fourierdlem33  41266  fourierdlem43  41276  fourierdlem65  41297  fourierdlem79  41311  issald  41457  iccpartrn  42380  bgoldbtbnd  42704  expnegico01  43305  dignnld  43394  reorelicc  43428