Theorem mpbir3and 1359

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

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

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 401  df-3an 1103

This theorem is referenced by:  2ellim  8483  canthwelem  10634  intwun  10719  tskwun  10768  gruwun  10797  ixxss1  13389  ixxss2  13390  ixxss12  13391  ixxub  13392  ixxlb  13393  elicod  13421  ubioc1  13425  lbico1  13426  lbicc2  13490  ubicc2  13491  difreicc  13510  supicc  13527  nnge2recico01  13533  modelico  13913  zmodfz  13925  addmodid  13954  dfrtrcl2  15098  phicl2  16826  4sqlem12  17015  isfuncd  17921  idfucl  17937  cofucl  17944  invfuc  18033  cnvps  18633  psss  18635  issubmd  18863  mndissubm  18864  submid  18867  subsubm  18874  0subm  18875  mhmima  18883  mhmeql  18884  gsumwspan  18904  frmdsssubm  18919  sursubmefmnd  18954  injsubmefmnd  18955  issubgrpd2  19208  grpissubg  19212  subgint  19216  nmzsubg  19230  eqger  19245  eqgcpbl  19249  cycsubm  19272  cycsubgcl  19276  ghmrn  19298  ghmpreima  19307  gastacl  19378  cntzsubm  19407  sylow2blem1  19689  lsmsubm  19722  torsubg  19923  oddvdssubg  19924  dmdprdd  20070  dprdsubg  20095  dprdres  20099  unitsubm  20467  cntzsubrng  20651  subrgsubm  20669  subrgugrp  20675  subrgint  20679  cntzsubr  20690  issubdrg  20862  lsssubg  21057  islmhm2  21138  pj1lmhm  21200  islbs2  21257  islbs3  21258  lbsextlem4  21264  issubrgd  21289  lidlsubg  21327  2idlcpblrng  21389  isphld  21783  mplsubglem  22127  mplsubrg  22133  mplind  22200  mhpsubg  22295  dmatsgrp  22635  dmatsrng  22637  scmatsgrp  22655  scmatsrng  22656  scmatsgrp1  22658  scmatsrng1  22659  cpmatsubgpmat  22856  cpmatsrgpmat  22857  lmcnp  23440  isufil2  24044  ufileu  24055  filufint  24056  fmfnfm  24094  flimclslem  24120  fclsfnflim  24163  flimfnfcls  24164  fclscmp  24166  clssubg  24245  tgpconncompeqg  24248  tgpconncomp  24249  qustgpopn  24256  tgptsmscls  24286  xmeter  24569  metust  24694  tgqioo  24936  zcld  24950  iccntr  24958  icccmplem2  24960  icccmplem3  24961  reconnlem1  24963  reconnlem2  24964  xrge0tsms  24971  cnheiborlem  25092  om1addcl  25171  pi1blem  25177  pi1grplem  25187  pi1inv  25190  pi1xfr  25193  pi1xfrcnvlem  25194  pi1coghm  25199  cmetcaulem  25426  ivthlem2  25590  ivthlem3  25591  ovolicc2lem2  25656  ovolicc2lem5  25659  opnmbllem  25739  volcn  25744  ismbf3d  25792  mbfi1fseqlem6  25858  itg2const2  25879  i1fibl  25946  ibladd  25959  bddiblnc  25980  ditgsplitlem  25998  dvferm1lem  26122  dvferm2lem  26124  dvlip2  26133  dvivthlem1  26146  dvne0  26149  lhop1lem  26151  lhop1  26152  lhop  26154  dvcnvrelem1  26155  dvcnvrelem2  26156  dvcnvre  26157  ftc1lem1  26173  itgsubst  26187  aaliou3lem2  26483  psercnlem2  26563  efif1olem2  26684  logtayl  26801  log2tlbnd  27086  xrlimcnp  27109  pntibndlem2  27731  pntlemj  27743  pntleml  27751  bday0b  27982  cuteq0  27984  cuteq1  27986  madebdaylemlrcut  28068  cofcut1  28089  oncutlt  28433  trgcgr  28761  hlid  28857  hltr  28858  btwnhl1  28860  btwnhl2  28861  hlcgrex  28864  mirhl  28932  mirbtwnhl  28933  mirhl2  28934  hlpasch  29013  lnopp2hpgb  29020  cgrahl  29111  axlowdim  29277  uhgrissubgr  29591  egrsubgr  29593  uhgrspansubgr  29607  uhgrspan1  29619  cusgrrusgr  29897  wlkonwlk  29976  wlkonwlk1l  29977  wlkres  29984  wlkp1  29995  wlkd  30000  lfgriswlk  30002  wwlksnextinj  30214  2wlkond  30252  wpthswwlks2on  30279  0wlkon  30437  1wlkd  30458  1pthond  30461  eliccelico  33088  elicoelioo  33089  xrge0tsmsd  33359  tpr2rico  34268  measinb  34577  cntmeas  34582  dya2icoseg  34633  sibf0  34690  sibfof  34696  pfxwlk  35570  revwlk  35571  resconn  35692  cvmsss2  35720  cvmliftlem10  35740  mrsubco  35967  cgrextend  36454  cgr3rflx  36500  cgrxfr  36501  btwnconn1lem4  36536  btwnconn1lem8  36540  btwnconn1lem11  36543  bj-pinftynminfty  37815  bj-rveccmod  37890  iooelexlt  37952  opnmbllem0  38251  ibladdnc  38272  ftc1anc  38296  isbnd3  38379  prdsbnd  38388  rngomndo  38530  isgrpda  38550  rngohomco  38569  rngoisocnv  38576  rngoidl  38619  0idl  38620  intidl  38624  unichnidl  38626  keridl  38627  smprngopr  38647  lshpnel2N  39705  lkrshp  39825  4atexlemex2  40791  4atex  40796  cdleme0moN  40945  istendod  41482  dihlspsnat  42053  dochsatshp  42171  mon1psubm  43874  iocinico  43887  dfrtrcl3  44407  eliood  46162  eliccd  46168  eliocd  46171  limciccioolb  46285  limcicciooub  46299  icccncfext  46549  iblspltprt  46635  itgspltprt  46641  fourierdlem1  46770  fourierdlem4  46773  fourierdlem32  46801  fourierdlem33  46802  fourierdlem43  46812  fourierdlem65  46833  fourierdlem79  46847  prsal  46980  issald  46995  flmrecm1  48025  iccpartrn  48124  fpprwpprb  48450  bgoldbtbnd  48519  upgrimwlk  48612  upgrimpths  48619  gpgedgvtx0  48771  gpgedgvtx1  48772  gpgprismgr4cycllem11  48815  smprngprmrng  49049  expnegico01  49243  dignnld  49328  reorelicc  49435