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

Theorem 3impia 1184
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 1181 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  mopick2  2348  3gencl  3004  mob2  3139  moi  3142  reupick3  3635  disjne  3724  disji2  4279  disji  4280  tz7.2  4704  ordintdif  4768  sofld  5286  funopg  5450  fvun1  5762  fvopab6  5796  fvcofneq  5851  fprg  5891  isores3  6026  ovmpt4g  6213  ovmpt2s  6214  ov2gf  6215  suppss2OLD  6315  ofrval  6330  sorpssuni  6369  sorpssint  6370  poxp  6684  suppss2  6723  smoel  6821  smoord  6826  smogt  6828  oaass  7000  oewordi  7030  oeoalem  7035  oeoelem  7037  nnawordi  7060  nnaass  7061  qsel  7179  xpdom3  7409  onsdominel  7460  mapdom3  7483  fisseneq  7524  cantnflem1  7897  cantnflem1OLD  7920  cfslbn  8436  cfsmolem  8439  cfcoflem  8441  infpssrlem4  8475  fin23lem7  8485  fin23lem25  8493  isf34lem7  8548  hsmexlem2  8596  axcc3  8607  axdc4lem  8624  tskss  8925  gruss  8963  gruurn  8965  gruiun  8966  gruel  8970  gruen  8979  grudomon  8984  grothac  8997  axpre-sup  9336  axsup  9450  letrp1  10171  p1le  10172  lemul1a  10183  zextle  10715  zextlt  10716  btwnnz  10718  gtndiv  10719  uzind2  10734  fzind  10740  uzletr  10869  eluzsub  10890  zsupss  10944  xrltne  11137  qbtwnre  11169  qbtwnxr  11170  xlemul1a  11251  iccleub  11351  iccsplit  11418  uzsubsubfz  11471  elfz0fzfz0  11485  elfzo0le  11590  fzonmapblen  11592  fzofzim  11593  ceile  11688  modadd1  11745  modmul1  11752  modirr  11769  expcl2lem  11877  expclzlem  11889  expnegz  11898  leexp2r  11921  bcval4  12083  bccmpl  12085  hashbnd  12109  ccatval2  12277  wrdl1s1  12301  swrdccatin1  12374  repswswrd  12422  absexpz  12794  climbdd  13149  iseraltlem2  13160  znnenlem  13494  dvdsle  13578  divalgb  13608  ndvdssub  13611  dvdsgcd  13727  rplpwr  13740  qredeq  13792  prmdvdsexpr  13802  nnnn0modprm0  13874  pcexp  13926  prmpwdvds  13965  ramcl  14090  cshwshashlem3  14124  cshwrepswhash1  14129  elrestr  14367  xpscfv  14500  mreintcl  14533  mremre  14542  mrieqv2d  14577  prstr  15103  drsdirfi  15108  latnlej  15238  latnlej2  15241  acsdrsel  15337  acsdrscl  15340  mrelatglb  15354  mrelatlub  15356  grpinvnz  15597  mulgneg2  15654  gsmsymgrfix  15933  f1omvdco2  15954  symggen  15976  odcl2  16066  odhash3  16075  lsmss1  16163  lsmss2  16165  efgred  16245  efgcpbl  16253  ablfacrp  16567  ablfac1eu  16574  ablfaclem3  16588  dvdsrmul1  16745  dvdsunit  16755  irredmul  16801  lmodlema  16953  ply1scln0  17743  psgnodpmr  18020  lindsss  18253  lindfmm  18256  mdetunilem7  18424  slesolinv  18486  cramerimplem3  18491  riinopn  18521  clsndisj  18679  cnpf2  18854  hausnei2  18957  cmpcov  18992  cmpfii  19012  bwthOLD  19014  uncon  19033  t1conperf  19040  nrmr0reg  19322  fbfinnfr  19414  filuni  19458  alexsubALT  19623  tmdgsum  19666  cuspcvg  19876  mopni  20067  isngp4  20203  metdsre  20429  iimulcl  20509  phtpc01  20568  clmmulg  20665  cfilucfil4OLD  20831  cfilucfil4  20832  bcthlem5  20839  bcth  20840  bcth3  20842  itg1le  21191  itg2le  21217  bddmulibl  21316  dvnres  21405  cpnord  21409  dvnfre  21426  deg1ge  21570  dgr1term  21727  aaliou3lem2  21809  sincosq1lem  21959  cxpge0  22128  cxpmul2  22134  logrec  22215  sqfpc  22475  bcmono  22616  pntrmax  22813  qabvexp  22875  ostth2lem2  22883  ax5seglem4  23178  axeuclidlem  23208  grpoasscan1  23724  gxnn0neg  23750  gxnn0suc  23751  gxcl  23752  gxneg  23753  gxcom  23756  gxinv  23757  gxsuc  23759  gxnn0add  23761  gxadd  23762  gxnn0mul  23764  gxmul  23765  gxdi  23783  nvs  24050  nvtri  24058  nmlno0  24195  nmlnoubi  24196  ubth  24274  hlipgt0  24315  ocnel  24701  elspansn2  24970  elspansn3  24975  normcan  24979  pjoml2  25014  lecm  25020  osum  25048  nmbdfnlb  25454  leopmul  25538  hstpyth  25633  cvnbtwn  25690  ssmd1  25715  ssmd2  25716  ssdmd1  25717  ssdmd2  25718  cvmd  25740  cvdmd  25741  superpos  25758  disji2f  25921  disjif  25922  disjif2  25925  bcm1n  26079  omndadd  26169  ogrpaddlt  26181  archiabl  26215  slmdlema  26219  eulerpartlemb  26751  sgn3da  26924  cvmsdisj  27159  cvmlift2lem12  27203  binomfallfac  27544  poseq  27714  nodenselem8  27829  nofulllem4  27846  lineintmo  28188  bddiblnc  28462  areacirc  28489  nn0prpwlem  28517  nn0prpw  28518  neibastop2lem  28581  incsequz  28644  mettrifi  28653  ismtybnd  28706  heiborlem1  28710  rngoisocnv  28787  risci  28793  incssnn0  29047  pell14qrexpcl  29208  pell14qrgap  29216  congadd  29309  acongsym  29319  acongtr  29321  dvdsacongtr  29327  jm2.19lem3  29340  jm2.19lem4  29341  jm2.26lem3  29350  2f1fvneq  30143  uzuzle  30190  elfzelfzlble  30209  subsubelfzo0  30210  el2fzo  30212  fzosplitprm1  30224  elovmpt2wrd  30256  edgwlk  30294  usgra2pthspth  30295  usgra2wlkspthlem1  30296  usgra2wlkspthlem2  30297  wwlknimp  30321  wlkiswwlk1  30324  wlkiswwlk2  30331  wwlknext  30356  usg2wotspth  30403  wwlkext2clwwlk  30465  erclwwlktr0  30479  erclwwlkeqlen  30482  erclwwlksym  30484  erclwwlktr  30485  difelfznle  30488  erclwwlkneqlen  30498  erclwwlknsym  30500  erclwwlkntr  30501  usgfiregdegfi  30528  rusgraprop2  30554  rusgraprop3  30555  wwlkextproplem2  30561  rusgranumwlk  30575  4cycl2vnunb  30609  usgn0fidegnn0  30622  fsuppmapnn0fiub0  30801  dmatelnd  30875  scmatsubcl  30884  scmatmulcl  30886  mdet0  30933  mdetdiaglem  30935  lincscmcl  30966  lindslinindimp2lem4  30995  lincresunit2  31012  lincresunit3  31015  bi13impia  31192  3impcombi  31550  lfl1  32715  lkrlsp2  32748  omlfh3N  32904  cvrnbtwn  32916  cvrnbtwn2  32920  cvrnbtwn4  32924  cvlexch3  32977  cvlexch4N  32978  cvlatexchb1  32979  2llnne2N  33052  atcvrj0  33072  cvrat2  33073  ps-1  33121  3atlem5  33131  islln2a  33161  lplnriaN  33194  lplnribN  33195  llncvrlpln2  33201  lplncvrlvol2  33259  psubatN  33399  pmapglb2N  33415  pmapglb2xN  33416  2llnma1b  33430  paddasslem17  33480  pmod2iN  33493  pmodl42N  33495  hlmod1i  33500  atmod1i1  33501  atmod1i2  33503  llnmod1i2  33504  pclcmpatN  33545  osumcllem8N  33607  pexmidlem3N  33616  pl42lem4N  33626  4atexlem7  33719  ltrnnid  33780  cdlemc4  33838  cdleme32a  34085  cdlemeg46gfre  34176  cdlemf2  34206  cdlemg4c  34256  trlcoat  34367  tendovalco  34409  tendoeq2  34418  cdlemk36  34557  diael  34688  diatrl  34689  dicelval1stN  34833  dicelval2nd  34834  dihlspsnat  34978  dochkr1  35123  lcfrlem9  35195  mapdh8e  35429  hdmapval0  35481  hgmapval0  35540
  Copyright terms: Public domain W3C validator