Theorem mpbir3and 1245

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	|- ( ph -> ch )
mpbir3and.2	|- ( ph -> th )
mpbir3and.3	|- ( ph -> ta )
mpbir3and.4	|- ( ph -> ( ps <-> ( ch /\ th /\ ta ) ) )

Assertion

Ref	Expression
mpbir3and	|- ( ph -> ps )

Proof of Theorem mpbir3and

Step	Hyp	Ref	Expression
1		mpbir3and.1	. . 3 |- ( ph -> ch )
2		mpbir3and.2	. . 3 |- ( ph -> th )
3		mpbir3and.3	. . 3 |- ( ph -> ta )
4	1, 2, 3	3jca 1242	. 2 |- ( ph -> ( ch /\ th /\ ta ) )
5		mpbir3and.4	. 2 |- ( ph -> ( ps <-> ( ch /\ th /\ ta ) ) )
6	4, 5	mpbird 247	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 196   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  canthwelem  9472  intwun  9557  tskwun  9606  gruwun  9635  ixxss1  12193  ixxss2  12194  ixxss12  12195  ixxub  12196  ixxlb  12197  elicod  12224  ubioc1  12227  lbico1  12228  lbicc2  12288  ubicc2  12289  difreicc  12304  supicc  12320  modelico  12680  zmodfz  12692  addmodid  12718  dfrtrcl2  13802  phicl2  15473  4sqlem12  15660  isfuncd  16525  idfucl  16541  cofucl  16548  invfuc  16634  cnvps  17212  psss  17214  issubmd  17349  submid  17351  subsubm  17357  mhmima  17363  mhmeql  17364  gsumwspan  17383  frmdsssubm  17398  issubgrpd2  17610  grpissubg  17614  subgint  17618  0subg  17619  cycsubgcl  17620  nmzsubg  17635  eqger  17644  eqgcpbl  17648  ghmrn  17673  ghmpreima  17682  gastacl  17742  cntzsubm  17768  sylow2blem1  18035  lsmsubm  18068  torsubg  18257  oddvdssubg  18258  dmdprdd  18398  dprdsubg  18423  dprdres  18427  unitsubm  18670  subrgsubm  18793  subrgugrp  18799  subrgint  18802  issubdrg  18805  cntzsubr  18812  lsssubg  18957  islmhm2  19038  pj1lmhm  19100  islbs2  19154  islbs3  19155  lbsextlem4  19161  issubrngd2  19189  lidlsubg  19215  2idlcpbl  19234  mplsubglem  19434  mplsubrg  19440  mplind  19502  isphld  19999  dmatsgrp  20305  dmatsrng  20307  scmatsgrp  20325  scmatsrng  20326  scmatsgrp1  20328  scmatsrng1  20329  cpmatsubgpmat  20525  cpmatsrgpmat  20526  lmcnp  21108  isufil2  21712  ufileu  21723  filufint  21724  fmfnfm  21762  flimclslem  21788  fclsfnflim  21831  flimfnfcls  21832  fclscmp  21834  clssubg  21912  tgpconncompeqg  21915  tgpconncomp  21916  qustgpopn  21923  tgptsmscls  21953  xmeter  22238  metust  22363  tgqioo  22603  zcld  22616  iccntr  22624  icccmplem2  22626  icccmplem3  22627  reconnlem1  22629  reconnlem2  22630  xrge0tsms  22637  cnheiborlem  22753  om1addcl  22833  pi1blem  22839  pi1grplem  22849  pi1inv  22852  pi1xfr  22855  pi1xfrcnvlem  22856  pi1coghm  22861  cmetcaulem  23086  ivthlem2  23221  ivthlem3  23222  ovolicc2lem2  23286  ovolicc2lem5  23289  opnmbllem  23369  volcn  23374  ismbf3d  23421  mbfi1fseqlem6  23487  itg2const2  23508  i1fibl  23574  ibladd  23587  ditgsplitlem  23624  dvferm1lem  23747  dvferm2lem  23749  dvlip2  23758  dvivthlem1  23771  dvne0  23774  lhop1lem  23776  lhop1  23777  lhop  23779  dvcnvrelem1  23780  dvcnvrelem2  23781  dvcnvre  23782  ftc1lem1  23798  itgsubst  23812  aaliou3lem2  24098  psercnlem2  24178  efif1olem2  24289  logtayl  24406  log2tlbnd  24672  xrlimcnp  24695  pntibndlem2  25280  pntlemj  25292  pntleml  25300  trgcgr  25411  axlowdim  25841  uhgrissubgr  26167  egrsubgr  26169  uhgrspansubgr  26183  uhgrspan1  26195  nbgr2vtx1edg  26246  nbuhgr2vtx1edgb  26248  cusgrexi  26339  structtocusgr  26342  cusgrrusgr  26477  wlkonwlk  26558  wlkonwlk1l  26559  wlkres  26567  wlkp1  26578  wlkd  26583  lfgriswlk  26585  wwlksnextinj  26794  2wlkond  26833  wpthswwlks2on  26854  0wlkon  26981  1wlkd  27001  1pthond  27004  eliccelico  29539  elicoelioo  29540  xrge0tsmsd  29785  tpr2rico  29958  measinb  30284  cntmeas  30289  dya2icoseg  30339  sibf0  30396  sibfof  30402  resconn  31228  cvmsss2  31256  cvmliftlem10  31276  mrsubco  31418  cgrextend  32115  cgr3rflx  32161  cgrxfr  32162  btwnconn1lem4  32197  btwnconn1lem8  32201  btwnconn1lem11  32204  bj-pinftynminfty  33114  iooelexlt  33210  opnmbllem0  33445  ibladdnc  33467  bddiblnc  33480  ftc1anc  33493  isbnd3  33583  prdsbnd  33592  rngomndo  33734  isgrpda  33754  rngohomco  33773  rngoisocnv  33780  rngoidl  33823  0idl  33824  intidl  33828  unichnidl  33830  keridl  33831  smprngopr  33851  lshpnel2N  34272  lkrshp  34392  4atexlemex2  35357  4atex  35362  cdleme0moN  35512  istendod  36050  dihlspsnat  36622  dochsatshp  36740  mon1psubm  37784  iocinico  37797  dfrtrcl3  38025  eliood  39720  eliccd  39726  eliocd  39730  limciccioolb  39853  limcicciooub  39869  icccncfext  40100  iblspltprt  40189  itgspltprt  40195  fourierdlem1  40325  fourierdlem4  40328  fourierdlem32  40356  fourierdlem33  40357  fourierdlem43  40367  fourierdlem65  40388  fourierdlem79  40402  issald  40551  iccpartrn  41366  bgoldbtbnd  41697  expnegico01  42308  dignnld  42397