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

Theorem 3impia 1191
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 432 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1188 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  mopick2  2293  3gencl  3066  mob2  3204  moi  3207  reupick3  3708  disjne  3788  disji2  4354  disji  4355  tz7.2  4777  ordintdif  4841  sofld  5364  funopg  5528  fvun1  5845  fvopab6  5882  fveqressseq  5929  fvcofneq  5941  fprg  5982  isores3  6132  ovmpt4g  6324  ovmpt2s  6325  ov2gf  6326  suppss2OLD  6429  ofrval  6449  sorpssuni  6488  sorpssint  6489  poxp  6811  suppss2  6852  smoel  6949  smoord  6954  smogt  6956  oaass  7128  oewordi  7158  oeoalem  7163  oeoelem  7165  nnawordi  7188  nnaass  7189  qsel  7308  xpdom3  7534  onsdominel  7585  mapdom3  7608  fisseneq  7647  cantnflem1  8021  cantnflem1OLD  8044  cfslbn  8560  cfsmolem  8563  cfcoflem  8565  infpssrlem4  8599  fin23lem7  8609  fin23lem25  8617  isf34lem7  8672  hsmexlem2  8720  axcc3  8731  axdc4lem  8748  tskss  9047  gruss  9085  gruurn  9087  gruiun  9088  gruel  9092  gruen  9101  grudomon  9106  grothac  9119  axpre-sup  9457  axsup  9571  letrp1  10301  p1le  10302  lemul1a  10313  zextle  10853  zextlt  10854  btwnnz  10856  gtndiv  10857  uzind2  10872  fzind  10877  eluzsub  11030  zsupss  11090  xrltne  11287  qbtwnre  11319  qbtwnxr  11320  xlemul1a  11401  iccleub  11501  iccsplit  11574  uzsubsubfz  11628  elfz0fzfz0  11701  difelfznle  11711  elfzo0le  11761  fzonmapblen  11763  fzofzim  11764  fzosplitprm1  11818  ceile  11876  modadd1  11934  muladdmodid  11937  modmul1  11943  modirr  11960  fsuppmapnn0fiub0  12002  expcl2lem  12081  expclzlem  12093  expnegz  12103  leexp2r  12126  bcval4  12287  bccmpl  12289  hashbnd  12313  elovmpt2wrd  12491  ccatval2  12505  wrdl1s1  12531  ccat2s1fvw  12551  swrdsb0eq  12583  swrdccatin1  12619  repswswrd  12667  cshwcsh2id  12707  absexpz  13140  climbdd  13496  iseraltlem2  13507  znnenlem  13947  dvdsle  14033  divalgb  14064  ndvdssub  14067  dvdsgcd  14183  rplpwr  14196  qredeq  14249  prmdvdsexpr  14259  nnnn0modprm0  14333  pcexp  14385  prmpwdvds  14424  ramcl  14549  cshwshashlem3  14584  cshwrepswhash1  14589  elrestr  14836  xpscfv  14969  mreintcl  15002  mremre  15011  mrieqv2d  15046  initoeu2lem1  15410  funcestrcsetclem9  15534  funcsetcestrclem9  15549  prstr  15679  drsdirfi  15684  latnlej  15815  latnlej2  15818  acsdrsel  15914  acsdrscl  15917  mrelatglb  15931  mrelatlub  15933  isnmgm  15993  mndassOLD  16049  grpinvnz  16226  mulgneg2  16286  gsmsymgrfix  16570  f1omvdco2  16590  symggen  16612  odcl2  16704  odhash3  16713  lsmss1  16801  lsmss2  16803  efgred  16883  efgcpbl  16891  ablfacrp  17230  ablfac1eu  17237  ablfaclem3  17251  dvdsrmul1  17415  dvdsunit  17425  irredmul  17471  lmodlema  17630  ply1scln0  18445  psgnodpmr  18717  lindsss  18944  lindfmm  18947  dmatelnd  19083  mdetdiaglem  19185  mdet0  19193  mdetunilem7  19205  slesolinv  19267  cramerimplem3  19272  cpmatpmat  19296  m2cpminvid2lem  19340  chfacfscmul0  19444  chfacfpmmul0  19448  riinopn  19502  clsndisj  19662  cnpf2  19837  hausnei2  19940  cmpcov  19975  cmpfii  19995  uncon  20015  t1conperf  20022  nrmr0reg  20335  fbfinnfr  20427  filuni  20471  alexsubALT  20636  tmdgsum  20679  cuspcvg  20889  mopni  21080  isngp4  21216  metdsre  21442  iimulcl  21522  phtpc01  21581  clmmulg  21678  cfilucfil4OLD  21844  cfilucfil4  21845  bcthlem5  21852  bcth  21853  bcth3  21855  itg1le  22205  itg2le  22231  bddmulibl  22330  dvnres  22419  cpnord  22423  dvnfre  22440  deg1ge  22584  dgr1term  22742  aaliou3lem2  22824  sincosq1lem  22975  cxpge0  23151  cxpmul2  23157  logrec  23221  sqfpc  23528  bcmono  23669  pntrmax  23866  qabvexp  23928  ostth2lem2  23936  ax5seglem4  24356  axeuclidlem  24386  edgwlk  24652  usgra2wlkspthlem1  24740  usgra2wlkspthlem2  24741  wwlknimp  24808  wlkiswwlk1  24811  wlkiswwlk2  24818  wwlknext  24845  wwlkextproplem2  24863  wwlkext2clwwlk  24924  erclwwlkeqlen  24933  erclwwlksym  24935  erclwwlktr  24936  erclwwlkneqlen  24945  erclwwlknsym  24947  erclwwlkntr  24948  usg2wotspth  25005  usgfiregdegfi  25032  rusgraprop2  25063  rusgraprop3  25064  rusgranumwlk  25078  4cycl2vnunb  25138  usgn0fidegnn0  25150  grpoasscan1  25356  gxnn0neg  25382  gxnn0suc  25383  gxcl  25384  gxneg  25385  gxcom  25388  gxinv  25389  gxsuc  25391  gxnn0add  25393  gxadd  25394  gxnn0mul  25396  gxmul  25397  gxdi  25415  nvs  25682  nvtri  25690  nmlno0  25827  nmlnoubi  25828  ubth  25906  hlipgt0  25947  ocnel  26333  elspansn2  26602  elspansn3  26607  normcan  26611  pjoml2  26646  lecm  26652  osum  26680  nmbdfnlb  27085  leopmul  27169  hstpyth  27264  cvnbtwn  27321  ssmd1  27346  ssmd2  27347  ssdmd1  27348  ssdmd2  27349  cvmd  27371  cvdmd  27372  superpos  27389  disji2f  27567  disjif  27568  disjif2  27571  padct  27695  ffs2  27701  bcm1n  27753  omndadd  27849  ogrpaddlt  27861  archiabl  27895  slmdlema  27899  eulerpartlemb  28490  sgn3da  28663  cvmsdisj  28904  cvmlift2lem12  28948  binomfallfac  29329  poseq  29498  nodenselem8  29613  nofulllem4  29630  lineintmo  29960  bddiblnc  30251  areacirc  30278  nn0prpwlem  30306  nn0prpw  30307  neibastop2lem  30344  incsequz  30407  mettrifi  30416  ismtybnd  30469  heiborlem1  30473  rngoisocnv  30550  risci  30556  incssnn0  30809  pell14qrexpcl  30968  pell14qrgap  30976  congadd  31069  acongsym  31079  acongtr  31081  dvdsacongtr  31087  jm2.19lem3  31099  jm2.19lem4  31100  jm2.26lem3  31109  lcmgcdlem  31380  ioogtlb  31694  iocgtlb  31701  iocleub  31702  icogelb  31708  icoltub  31711  iooltub  31714  limclner  31823  pfx2  32587  pfxccatpfx2  32603  2f1fvneq  32628  elfzelfzlble  32658  subsubelfzo0  32659  usgra2pthspth  32669  c0snmgmhm  32920  funcringcsetcALTV2lem9  33052  funcringcsetclem9ALTV  33075  lincscmcl  33233  lindslinindimp2lem4  33262  lincresunit2  33279  lincresunit3  33282  elfzolborelfzop1  33325  m1modmmod  33334  rege1logbzge0  33380  fllog2  33389  dignn0ldlem  33423  bi13impia  33590  3impcombi  33954  lfl1  35208  lkrlsp2  35241  omlfh3N  35397  cvrnbtwn  35409  cvrnbtwn2  35413  cvrnbtwn4  35417  cvlexch3  35470  cvlexch4N  35471  cvlatexchb1  35472  2llnne2N  35545  atcvrj0  35565  cvrat2  35566  ps-1  35614  3atlem5  35624  islln2a  35654  lplnriaN  35687  lplnribN  35688  llncvrlpln2  35694  lplncvrlvol2  35752  psubatN  35892  pmapglb2N  35908  pmapglb2xN  35909  2llnma1b  35923  paddasslem17  35973  pmod2iN  35986  pmodl42N  35988  hlmod1i  35993  atmod1i1  35994  atmod1i2  35996  llnmod1i2  35997  pclcmpatN  36038  osumcllem8N  36100  pexmidlem3N  36109  pl42lem4N  36119  4atexlem7  36212  ltrnnid  36273  cdlemc4  36332  cdleme32a  36580  cdlemeg46gfre  36671  cdlemf2  36701  cdlemg4c  36751  trlcoat  36862  tendovalco  36904  tendoeq2  36913  cdlemk36  37052  diael  37183  diatrl  37184  dicelval1stN  37328  dicelval2nd  37329  dihlspsnat  37473  dochkr1  37618  lcfrlem9  37690  mapdh8e  37924  hdmapval0  37976  hgmapval0  38035  relexpiidm  38240
  Copyright terms: Public domain W3C validator