MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3impia Structured version   Unicode version

Theorem 3impia 1179
Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
Hypothesis
Ref Expression
3impia.1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Assertion
Ref Expression
3impia  |-  ( (
ph  /\  ps  /\  ch )  ->  th )

Proof of Theorem 3impia
StepHypRef Expression
1 3impia.1 . . 3  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
21ex 434 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1176 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 960
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 185  df-an 371  df-3an 962
This theorem is referenced by:  mopick2  2346  3gencl  2995  mob2  3130  moi  3133  reupick3  3625  disjne  3714  disji2  4269  disji  4270  tz7.2  4693  ordintdif  4757  sofld  5276  funopg  5440  fvun1  5752  fvopab6  5786  fvcofneq  5841  fprg  5880  isores3  6015  ovmpt4g  6204  ovmpt2s  6205  ov2gf  6206  suppss2OLD  6306  ofrval  6321  sorpssuni  6360  sorpssint  6361  poxp  6675  suppss2  6714  smoel  6809  smoord  6814  smogt  6816  oaass  6990  oewordi  7020  oeoalem  7025  oeoelem  7027  nnawordi  7050  nnaass  7051  qsel  7169  xpdom3  7399  onsdominel  7450  mapdom3  7473  fisseneq  7514  cantnflem1  7887  cantnflem1OLD  7910  cfslbn  8426  cfsmolem  8429  cfcoflem  8431  infpssrlem4  8465  fin23lem7  8475  fin23lem25  8483  isf34lem7  8538  hsmexlem2  8586  axcc3  8597  axdc4lem  8614  tskss  8915  gruss  8953  gruurn  8955  gruiun  8956  gruel  8960  gruen  8969  grudomon  8974  grothac  8987  axpre-sup  9326  axsup  9440  letrp1  10161  p1le  10162  lemul1a  10173  zextle  10705  zextlt  10706  btwnnz  10708  gtndiv  10709  uzind2  10724  fzind  10730  uzletr  10859  eluzsub  10880  zsupss  10934  xrltne  11127  qbtwnre  11159  qbtwnxr  11160  xlemul1a  11241  iccleub  11341  iccsplit  11407  uzsubsubfz  11460  elfz0fzfz0  11474  elfzo0le  11576  fzonmapblen  11578  fzofzim  11579  ceile  11674  modadd1  11731  modmul1  11738  modirr  11755  expcl2lem  11863  expclzlem  11875  expnegz  11884  leexp2r  11907  bcval4  12069  bccmpl  12071  hashbnd  12095  ccatval2  12263  wrdl1s1  12287  swrdccatin1  12360  repswswrd  12408  absexpz  12780  climbdd  13135  iseraltlem2  13146  znnenlem  13479  dvdsle  13563  divalgb  13593  ndvdssub  13596  dvdsgcd  13712  rplpwr  13725  qredeq  13777  prmdvdsexpr  13787  nnnn0modprm0  13859  pcexp  13911  prmpwdvds  13950  ramcl  14075  cshwshashlem3  14109  cshwrepswhash1  14114  elrestr  14352  xpscfv  14485  mreintcl  14518  mremre  14527  mrieqv2d  14562  prstr  15088  drsdirfi  15093  latnlej  15223  latnlej2  15226  acsdrsel  15322  acsdrscl  15325  mrelatglb  15339  mrelatlub  15341  grpinvnz  15579  mulgneg2  15636  gsmsymgrfix  15915  f1omvdco2  15936  symggen  15958  odcl2  16048  odhash3  16057  lsmss1  16145  lsmss2  16147  efgred  16227  efgcpbl  16235  ablfacrp  16543  ablfac1eu  16550  ablfaclem3  16564  dvdsrmul1  16681  dvdsunit  16691  irredmul  16737  lmodlema  16879  ply1scln0  17643  psgnodpmr  17864  lindsss  18097  lindfmm  18100  mdetunilem7  18268  slesolinv  18330  cramerimplem3  18335  riinopn  18365  clsndisj  18523  cnpf2  18698  hausnei2  18801  cmpcov  18836  cmpfii  18856  bwthOLD  18858  uncon  18877  t1conperf  18884  nrmr0reg  19166  fbfinnfr  19258  filuni  19302  alexsubALT  19467  tmdgsum  19510  cuspcvg  19720  mopni  19911  isngp4  20047  metdsre  20273  iimulcl  20353  phtpc01  20412  clmmulg  20509  cfilucfil4OLD  20675  cfilucfil4  20676  bcthlem5  20683  bcth  20684  bcth3  20686  itg1le  21035  itg2le  21061  bddmulibl  21160  dvnres  21249  cpnord  21253  dvnfre  21270  deg1ge  21457  dgr1term  21614  aaliou3lem2  21696  sincosq1lem  21846  cxpge0  22015  cxpmul2  22021  logrec  22102  sqfpc  22362  bcmono  22503  pntrmax  22700  qabvexp  22762  ostth2lem2  22770  ax5seglem4  23003  axeuclidlem  23033  grpoasscan1  23549  gxnn0neg  23575  gxnn0suc  23576  gxcl  23577  gxneg  23578  gxcom  23581  gxinv  23582  gxsuc  23584  gxnn0add  23586  gxadd  23587  gxnn0mul  23589  gxmul  23590  gxdi  23608  nvs  23875  nvtri  23883  nmlno0  24020  nmlnoubi  24021  ubth  24099  hlipgt0  24140  ocnel  24526  elspansn2  24795  elspansn3  24800  normcan  24804  pjoml2  24839  lecm  24845  osum  24873  nmbdfnlb  25279  leopmul  25363  hstpyth  25458  cvnbtwn  25515  ssmd1  25540  ssmd2  25541  ssdmd1  25542  ssdmd2  25543  cvmd  25565  cvdmd  25566  superpos  25583  disji2f  25747  disjif  25748  disjif2  25751  bcm1n  25904  omndadd  25995  ogrpaddlt  26007  archiabl  26041  slmdlema  26070  eulerpartlemb  26601  sgn3da  26774  cvmsdisj  27009  cvmlift2lem12  27053  binomfallfac  27393  poseq  27563  nodenselem8  27678  nofulllem4  27695  lineintmo  28037  bddiblnc  28308  areacirc  28335  nn0prpwlem  28363  nn0prpw  28364  neibastop2lem  28427  incsequz  28490  mettrifi  28499  ismtybnd  28552  heiborlem1  28556  rngoisocnv  28633  risci  28639  incssnn0  28894  pell14qrexpcl  29055  pell14qrgap  29063  congadd  29156  acongsym  29166  acongtr  29168  dvdsacongtr  29174  jm2.19lem3  29187  jm2.19lem4  29188  jm2.26lem3  29197  areaquad  29439  2f1fvneq  29991  uzuzle  30038  elfzelfzlble  30057  subsubelfzo0  30058  el2fzo  30060  fzosplitprm1  30072  elovmpt2wrd  30104  edgwlk  30142  usgra2pthspth  30143  usgra2wlkspthlem1  30144  usgra2wlkspthlem2  30145  wwlknimp  30169  wlkiswwlk1  30172  wlkiswwlk2  30179  wwlknext  30204  usg2wotspth  30251  wwlkext2clwwlk  30313  erclwwlktr0  30327  erclwwlkeqlen  30330  erclwwlksym  30332  erclwwlktr  30333  difelfznle  30336  erclwwlkneqlen  30346  erclwwlknsym  30348  erclwwlkntr  30349  usgfiregdegfi  30376  rusgraprop2  30402  rusgraprop3  30403  wwlkextproplem2  30409  rusgranumwlk  30423  4cycl2vnunb  30457  usgn0fidegnn0  30470  dmatelnd  30666  scmatsubcl  30675  scmatmulcl  30677  mdet0  30682  mdetdiaglem  30684  lincscmcl  30715  lindslinindimp2lem4  30744  lincresunit2  30761  lincresunit3  30764  bi13impia  30933  3impcombi  31292  lfl1  32328  lkrlsp2  32361  omlfh3N  32517  cvrnbtwn  32529  cvrnbtwn2  32533  cvrnbtwn4  32537  cvlexch3  32590  cvlexch4N  32591  cvlatexchb1  32592  2llnne2N  32665  atcvrj0  32685  cvrat2  32686  ps-1  32734  3atlem5  32744  islln2a  32774  lplnriaN  32807  lplnribN  32808  llncvrlpln2  32814  lplncvrlvol2  32872  psubatN  33012  pmapglb2N  33028  pmapglb2xN  33029  2llnma1b  33043  paddasslem17  33093  pmod2iN  33106  pmodl42N  33108  hlmod1i  33113  atmod1i1  33114  atmod1i2  33116  llnmod1i2  33117  pclcmpatN  33158  osumcllem8N  33220  pexmidlem3N  33229  pl42lem4N  33239  4atexlem7  33332  ltrnnid  33393  cdlemc4  33451  cdleme32a  33698  cdlemeg46gfre  33789  cdlemf2  33819  cdlemg4c  33869  trlcoat  33980  tendovalco  34022  tendoeq2  34031  cdlemk36  34170  diael  34301  diatrl  34302  dicelval1stN  34446  dicelval2nd  34447  dihlspsnat  34591  dochkr1  34736  lcfrlem9  34808  mapdh8e  35042  hdmapval0  35094  hgmapval0  35153
  Copyright terms: Public domain W3C validator