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

Theorem 3imp 1145
Description: Importation inference. (Contributed by NM, 8-Apr-1994.)
Hypothesis
Ref Expression
3imp.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
3imp  |-  ( (
ph  /\  ps  /\  ch )  ->  th )

Proof of Theorem 3imp
StepHypRef Expression
1 df-3an 936 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
2 3imp.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 421 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
41, 3sylbi 187 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3impa  1146  3impb  1147  3impia  1148  3impib  1149  3com23  1157  3an1rs  1163  3imp1  1164  3impd  1165  syl3an2  1216  syl3an3  1217  3jao  1243  biimp3ar  1282  wefrc  4387  sotri2  5072  sotri3  5073  poxp  6227  riotasvdOLD  6348  smo11  6381  oawordri  6548  odi  6577  omass  6578  nndi  6621  nnmass  6622  undifixp  6852  isinf  7076  domunfican  7129  pr2nelem  7634  dfac8alem  7656  fin33i  7995  fin1a2lem10  8035  domtriomlem  8068  axdc3lem2  8077  axdc3lem4  8079  axdc4lem  8081  ttukeyg  8144  axdclem  8146  grupr  8419  nqereu  8553  squeeze0  9659  rpnnen1lem5  10346  supxrun  10634  mulexp  11141  expadd  11144  expmul  11147  bernneq  11227  facdiv  11300  leisorel  11398  prmfac1  12797  infpnlem1  12957  iscatd2  13583  joinle  14127  meetle  14134  clatleglb  14230  lmodvsdi2OLD  15653  lmodvsassOLD  15655  lsmcv  15894  psrvscafval  16135  fiinopn  16647  opnneissb  16851  cnpimaex  16986  regsep  17062  hausnei2  17081  cmpsublem  17126  cmpsub  17127  filufint  17615  blss  17972  mblsplit  18891  bcmono  20516  2sqlem10  20613  clmgm  20988  grpomndo  21013  chcompl  21822  spansncol  22147  hoaddsub  22396  sconpht  23760  relexpindlem  24036  funpsstri  24121  predpo  24184  and4as  24939  rspc2edv  24963  isunscov  25074  eqfnung2  25118  mapmapmap  25148  prl  25167  prl2  25169  prjmapcp2  25170  dfps2  25289  iscomb  25334  clfsebsr  25349  multinv  25422  multinvb  25423  zerdivemp1  25436  rngoridfz  25437  svs2  25487  truni3  25507  unint2t  25518  intopcoaconlem3b  25538  fisub  25554  cmptdst  25568  limptlimpr2lem2  25575  islimrs3  25581  islimrs4  25582  bwt2  25592  flfneicn  25625  lvsovso  25626  lvsovso2  25627  negveud  25668  negveudr  25669  issubcv  25670  clsmulcv  25682  distsava  25689  hdrmp  25706  cmpassoh  25801  imonclem  25813  ismonc  25814  cmpmon  25815  icmpmon  25816  iepiclem  25823  isepic  25824  propsrc  25868  tartarmap  25888  cmpmor  25975  clscnc  26010  pgapspf2  26053  lppotos  26144  bosser  26167  pdiveql  26168  imp5p  26220  cntotbnd  26520  rngoneglmul  26582  rngonegrmul  26583  zerdivemp1x  26586  pell14qrexpclnn0  26951  pell1qrgap  26959  aomclem2  27152  rngunsnply  27378  ee333  28268  jaoded  28332  3imp31  28333  3imp21  28334  e333  28508  suctrALTcf  28698  suctrALTcfVD  28699  a9e2ndeqALT  28708  bnj600  28951  atlex  29506  cvlexch1  29518  cvlsupr4  29535  cvlsupr5  29536  cvlsupr6  29537  2llnneN  29598  athgt  29645  llnle  29707  lplnle  29729  lvoli2  29770  pmaple  29950  dalawlem10  30069  dalawlem13  30072  dalawlem14  30073  dalaw  30075  lhp2lt  30190  ldilval  30302  cdleme50trn2  30740  cdlemf  30752  cdlemg18b  30868  tendotp  30950  tendospcanN  31213  dihmeetlem3N  31495  dvh4dimlem  31633
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator