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

Theorem 3impia 1202
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 435 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1199 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  mopick2  2340  3gencl  3119  mob2  3257  moi  3260  reupick3  3764  disjne  3844  disji2  4413  disji  4414  tz7.2  4838  sofld  5304  ordintdif  5491  funopg  5633  fvun1  5952  fvopab6  5990  fveqressseq  6033  fvcofneq  6045  fprg  6088  isores3  6241  ovmpt4g  6433  ovmpt2s  6434  ov2gf  6435  ofrval  6555  sorpssuni  6594  sorpssint  6595  poxp  6919  suppss2  6960  smoel  7087  smoord  7092  smogt  7094  oaass  7270  oewordi  7300  oeoalem  7305  oeoelem  7307  nnawordi  7330  nnaass  7331  qsel  7450  xpdom3  7676  onsdominel  7727  mapdom3  7750  fisseneq  7789  cantnflem1  8193  cfslbn  8695  cfsmolem  8698  cfcoflem  8700  infpssrlem4  8734  fin23lem7  8744  fin23lem25  8752  isf34lem7  8807  hsmexlem2  8855  axcc3  8866  axdc4lem  8883  tskss  9182  gruss  9220  gruurn  9222  gruiun  9223  gruel  9227  gruen  9236  grudomon  9241  grothac  9254  axpre-sup  9592  axsup  9708  letrp1  10446  p1le  10447  lemul1a  10458  infrelb  10596  zextle  11009  zextlt  11010  btwnnz  11012  gtndiv  11013  uzind2  11028  fzind  11033  eluzsub  11188  zsupss  11253  xrltne  11460  qbtwnre  11492  qbtwnxr  11493  xlemul1a  11574  icogelb  11686  iccleub  11690  iccsplit  11763  uzsubsubfz  11819  elfz0fzfz0  11893  difelfznle  11903  elfzo0le  11957  fzonmapblen  11959  fzofzim  11960  fzosplitprm1  12015  ceile  12073  modadd1  12131  muladdmodid  12134  modmul1  12140  modirr  12157  fsuppmapnn0fiub0  12202  expcl2lem  12281  expclzlem  12293  expnegz  12303  leexp2r  12327  bcval4  12489  bccmpl  12491  hashbnd  12518  elovmpt2wrd  12696  ccatval2  12710  wrdl1s1  12736  ccat2s1fvw  12756  swrdsb0eq  12788  swrdccatin1  12824  repswswrd  12872  cshwcsh2id  12912  absexpz  13347  climbdd  13713  iseraltlem2  13727  binomfallfac  14072  znnenlem  14242  dvdsle  14328  divalgb  14360  ndvdssub  14363  dvdsgcd  14482  rplpwr  14495  lcmgcdlem  14536  lcmfunsn  14579  qredeq  14625  prmdvdsexpr  14631  nnnn0modprm0  14711  pcexp  14763  prmpwdvds  14802  ramcl  14941  cshwshashlem3  15022  cshwrepswhash1  15027  elrestr  15277  xpscfv  15410  mreintcl  15443  mremre  15452  mrieqv2d  15487  initoeu2lem1  15851  funcestrcsetclem9  15975  funcsetcestrclem9  15990  prstr  16120  drsdirfi  16125  latnlej  16256  latnlej2  16259  acsdrsel  16355  acsdrscl  16358  mrelatglb  16372  mrelatlub  16374  isnmgm  16434  mndassOLD  16490  grpinvnz  16667  mulgneg2  16727  gsmsymgrfix  17011  f1omvdco2  17031  symggen  17053  odcl2  17145  odhash3  17154  lsmss1  17242  lsmss2  17244  efgred  17324  efgcpbl  17332  ablfacrp  17625  ablfac1eu  17632  ablfaclem3  17646  dvdsrmul1  17807  dvdsunit  17817  irredmul  17863  lmodlema  18022  ply1scln0  18810  psgnodpmr  19080  lindsss  19304  lindfmm  19307  dmatelnd  19443  mdetdiaglem  19545  mdet0  19553  mdetunilem7  19565  slesolinv  19627  cramerimplem3  19632  cpmatpmat  19656  m2cpminvid2lem  19700  chfacfscmul0  19804  chfacfpmmul0  19808  riinopn  19860  clsndisj  20013  cnpf2  20188  hausnei2  20291  cmpcov  20326  cmpfii  20346  uncon  20366  t1conperf  20373  nrmr0reg  20686  fbfinnfr  20778  filuni  20822  alexsubALT  20988  tmdgsum  21032  cuspcvg  21238  mopni  21429  isngp4  21547  metdsre  21772  iimulcl  21852  phtpc01  21911  clmmulg  22008  cfilucfil4  22173  bcthlem5  22180  bcth  22181  bcth3  22183  itg1le  22539  itg2le  22565  bddmulibl  22664  dvnres  22753  cpnord  22757  dvnfre  22774  deg1ge  22915  dgr1term  23073  aaliou3lem2  23155  sincosq1lem  23308  cxpge0  23484  cxpmul2  23490  logrec  23556  sqfpc  23918  bcmono  24059  pntrmax  24256  qabvexp  24318  ostth2lem2  24326  ax5seglem4  24799  axeuclidlem  24829  edgwlk  25095  usgra2wlkspthlem1  25183  usgra2wlkspthlem2  25184  wwlknimp  25251  wlkiswwlk1  25254  wlkiswwlk2  25261  wwlknext  25288  wwlkextproplem2  25306  wwlkext2clwwlk  25367  erclwwlkeqlen  25376  erclwwlksym  25378  erclwwlktr  25379  erclwwlkneqlen  25388  erclwwlknsym  25390  erclwwlkntr  25391  usg2wotspth  25448  usgfiregdegfi  25475  rusgraprop2  25506  rusgraprop3  25507  rusgranumwlk  25521  4cycl2vnunb  25581  usgn0fidegnn0  25593  grpoasscan1  25801  gxnn0neg  25827  gxnn0suc  25828  gxcl  25829  gxneg  25830  gxcom  25833  gxinv  25834  gxsuc  25836  gxnn0add  25838  gxadd  25839  gxnn0mul  25841  gxmul  25842  gxdi  25860  nvs  26127  nvtri  26135  nmlno0  26272  nmlnoubi  26273  ubth  26351  hlipgt0  26392  ocnel  26777  elspansn2  27046  elspansn3  27051  normcan  27055  pjoml2  27090  lecm  27096  osum  27124  nmbdfnlb  27529  leopmul  27613  hstpyth  27708  cvnbtwn  27765  ssmd1  27790  ssmd2  27791  ssdmd1  27792  ssdmd2  27793  cvmd  27815  cvdmd  27816  superpos  27833  disji2f  28017  disjif  28018  disjif2  28021  padct  28141  ffs2  28147  bcm1n  28198  omndadd  28298  ogrpaddlt  28310  archiabl  28344  slmdlema  28348  eulerpartlemb  29018  sgn3da  29191  cvmsdisj  29772  cvmlift2lem12  29816  br1steqg  30194  br2ndeqg  30195  poseq  30269  nodenselem8  30353  nofulllem4  30370  lineintmo  30700  nn0prpwlem  30754  nn0prpw  30755  neibastop2lem  30792  bddiblnc  31706  areacirc  31731  incsequz  31771  mettrifi  31780  ismtybnd  31833  heiborlem1  31837  rngoisocnv  31914  risci  31920  lfl1  32335  lkrlsp2  32368  omlfh3N  32524  cvrnbtwn  32536  cvrnbtwn2  32540  cvrnbtwn4  32544  cvlexch3  32597  cvlexch4N  32598  cvlatexchb1  32599  2llnne2N  32672  atcvrj0  32692  cvrat2  32693  ps-1  32741  3atlem5  32751  islln2a  32781  lplnriaN  32814  lplnribN  32815  llncvrlpln2  32821  lplncvrlvol2  32879  psubatN  33019  pmapglb2N  33035  pmapglb2xN  33036  2llnma1b  33050  paddasslem17  33100  pmod2iN  33113  pmodl42N  33115  hlmod1i  33120  atmod1i1  33121  atmod1i2  33123  llnmod1i2  33124  pclcmpatN  33165  osumcllem8N  33227  pexmidlem3N  33236  pl42lem4N  33246  4atexlem7  33339  ltrnnid  33400  cdlemc4  33459  cdleme32a  33707  cdlemeg46gfre  33798  cdlemf2  33828  cdlemg4c  33878  trlcoat  33989  tendovalco  34031  tendoeq2  34040  cdlemk36  34179  diael  34310  diatrl  34311  dicelval1stN  34455  dicelval2nd  34456  dihlspsnat  34600  dochkr1  34745  lcfrlem9  34817  mapdh8e  35051  hdmapval0  35103  hgmapval0  35162  incssnn0  35252  pell14qrexpcl  35411  pell14qrgap  35419  congadd  35512  acongsym  35522  acongtr  35524  dvdsacongtr  35530  jm2.19lem3  35542  jm2.19lem4  35543  jm2.26lem3  35552  relexpiidm  35925  bi13impia  36471  3impcombi  36834  ioogtlb  37167  iocgtlb  37174  iocleub  37175  icoltub  37182  iooltub  37185  limclner  37294  iccpartigtl  38117  wtgoldbnnsum4prm  38277  bgoldbnnsum3prm  38279  bgoldbtbndlem1  38280  bgoldbtbndlem3  38282  bgoldbtbndlem4  38283  bgoldbtbnd  38284  pfx2  38333  pfxccatpfx2  38349  2f1fvneq  38374  elfzelfzlble  38400  subsubelfzo0  38401  usgra2pthspth  38411  c0snmgmhm  38662  funcringcsetcALTV2lem9  38794  funcringcsetclem9ALTV  38817  lincscmcl  38975  lindslinindimp2lem4  39004  lincresunit2  39021  lincresunit3  39024  elfzolborelfzop1  39067  m1modmmod  39075  rege1logbzge0  39121  fllog2  39130  dignn0ldlem  39164
  Copyright terms: Public domain W3C validator